ARQNL 2014: Papers with Abstracts

Papers
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal and Stephan Merz 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.
A Logic for Verifying Metric Temporal Properties in Distributed Hybrid Systems Ping Hou and Yifei Chen 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.
Problem Libraries for Non-Classical Logics Jens Otten and Thomas Raths 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.
HOL Provers for First-order Modal Logics --- Experiments Christoph Benzmüller 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.
Proof Support for Common Logic Till Mossakowski, Mihai Codescu, Oliver Kutz, Christoph Lange and Michael Grüninger 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.
Embedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic Max Wisniewski and Alexander Steen 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.
Dialogues for proof search Jesse Alama 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.
Theorem Proving for Logic with Partial Functions Using Kleene Logic and Geometric Logic Hans De Nivelle 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.