ABSTRACT. The ARQNL Workshop provides a forum for researchers to present and discuss work on the development of proof calculi, automated theorem proving systems and model finders for all sorts of quantified non-classical logics.

The ARQNL Workshop proceedings can be downloaded at http://www.iltp.de/ARQNL-2014.

ABSTRACT. We present a syntactic abstraction method to reason about first-order modal logics by using theorem provers for standard first-order logic and for propositional modal logic.

ABSTRACT. We introduce a logic for specifying and verifying metric temporal properties of distributed hybrid systems that combines quantified differential dynamic logic (QdL) for reasoning about the possible behavior of distributed hybrid systems with metric temporal logic (MTL) for reasoning about the metric temporal behavior during their operation. For our combined logic, we generalize the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of QdL for distributed hybrid systems. On this basis, we provide a modular verification calculus that reduces correctness of metric temporal behavior of distributed hybrid systems to generic temporal reasoning and then non-temporal reasoning, and prove that we obtain a complete axiomatization relative to the non-temporal base logic QdL.

ABSTRACT. Problem libraries for automated theorem proving (ATP) systems play a crucial role when developing, testing, benchmarking and evaluating ATP systems for classical and non-classical logics. We provide an overview of existing problem libraries for some important non-classical logics, namely first-order intuitionistic and first-order modal logics. We suggest future plans to extend these existing libraries and discuss ideas for a general problem library platform for non-classical logics.

ABSTRACT. Higher-order automated theorem provers have been employed to automate first-order modal logics. Extending previous work, an experiment has been carried out to evaluate their collaborative and individual performances.

ABSTRACT. We present the theoretical background for an extension of the Heterogeneous Tool Set Hets that enables proof support for Common Logic. This is achieved via logic translations that relate Common Logic and some of its sublogics to already supported logics and automated theorem proving systems. We thus provide the first theorem proving support for Common Logic covering the full language, including the possibility of verifying meta-theoretical relationships between Common Logic theories.

ABSTRACT. In this paper, we present an embedding of higher-order nominal modal logic into classical higher-order logic, and study its automation. There exists no automated theorem prover for first-order or higher-order nominal logic at the moment, hence, this is the first automation for this kind of logic. In our work, we focus on nominal tense logic and have successfully proven some first theorems.

ABSTRACT. Dialogue games are a two-player semantics for a variety of logics, including intuitionistic and classical logic. Dialogues can be viewed as a kind of analytic calculus not unlike tableaux. Can dialogue games be an effective foundation for proof search in intuitionistic logic (both first-order and propositional)? We announce Kuno, an automated theorem prover for intuitionistic first-order logic based on dialogue games.

ABSTRACT. We introduce a theorem proving strategy for Partial Classical Logic (PCL) that is based on geometric logic. The strategy first translates PCL theories into sets of Kleene formulas. After that, the Kleene formulas are translated into 3-valued geometric logic. The resulting formulas can be refuted by an adaptation of geometric resolution.

The translation to Kleene logic does not only open the way to theorem proving, but it also sheds light on the relation between PCL, Kleene Logic, and classical logic.

ABSTRACT. An approach to the construction of computer-oriented first-order sequent logics (with or without equality) for both classical and intuitionistic cases and their modal extensions is developed. It exploits the original notions of admissibility and compatibility, which permits to avoid preliminary skolemization being a forbidden operation for a number of non-classical logics in general. Following the approach, the cut-free sequent (modal) calculi avoiding the dependence of inference search on different orders of quantifier rules applications are described. Results relating to the coextensivity of various sequent calculi are given. The research gives a way to the construction of computer-oriented quantifier-rule-free calculi for classical and intuitionistic logics and their modal extensions.