View: session overviewtalk overviewside by side with other conferences

10:15-10:45Coffee Break
10:50-11:00 Session 167: Opening
Location: FH, Seminarraum 138C
ARQNL Workshop - Opening

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.

11:00-13:00 Session 168: First-Order Modal Logics, Quantified Dynamic and Temporal Logic, Problem Libraries
Location: FH, Seminarraum 138C
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
SPEAKER: unknown

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

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
SPEAKER: Jens Otten

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

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.

13:00-14:30Lunch Break
14:30-16:00 Session 172E: Common Logic, Higher-Order Nominal Modal Logic, First-Order Intuitionistic Logic
Location: FH, Seminarraum 138C
Proof Support for Common Logic
SPEAKER: unknown

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
SPEAKER: unknown

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
SPEAKER: 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.

16:00-16:30Coffee Break
16:30-18:00 Session 175G: Logic with Partial Functions, First-Order Sequent Logics, Discussion
Location: FH, Seminarraum 138C
Theorem Proving for Logic with Partial Functions Using Kleene Logic and Geometric Logic

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.

Computer-oriented inference search in first-order sequent logics

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.

Open Discussion