Special Issue of the Conference "Automated Reasoning with Analytic Tableaux and Related Methods 2009"

2009

Editor: Martin Giese

This special issue of Logical Methods in Computer Science (LMCS) contains extended and revised versions of selected papers presented at the 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009) held July 6-10, 2009 in Oslo, Norway.

The programme committee of TABLEAUX 2009 received 44 submissions, out of which 21 research papers and 1 system description were accepted based on originality, technical soundness, presentation, and relevance. Based on the programme committee's assessment of the submissions, the seven best were selected and their authors invited to submit an extended and revised version. These submissions underwent a new and thorough review process, in accordance with the usual standards of LMCS. The accepted papers cover a broad range of logics (including modal, hybrid, conditional, and fuzzy logics) and tableau- and sequent-based methods (including display calculi, deep inference, single- and multi-conclusion sequent calculi).

The first paper of the issue is Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis by Silvio Ghilardi and Silvio Ranise. It considers the problem of proving safety properties of transition systems with array variables, which can model a wide range of infinite-state systems. The key idea is to compute the backward-reachable states from the unsafe states symbolically by representing states with formulae, and using an SMT solver as a sub-procedure in the backward reachability procedure.

This is followed by two papers concerned with generic cut elimination results. The paper On Constructive Connectives and Systems by Arnon Avron and Ori Lahav defines canonical inference rules and canonical systems in the framework of non-strict single-conclusion sequent systems and provides a general non-deterministic Kripke-style semantics. This is used to give a constructive sufficient and necessary coherence criterion for the validity of the strong cut-elimination theorem in such a system.

Dirk Pattinson and Lutz Schröder's contribution Generic Modal Cut Elimination Applied to Conditional Logics gives a general criterion for cut elimination in sequent calculi for propositional modal logics, that applies also to a wide variety of non-normal modal logics. The criterion's usefulness is illustrated on a variety of conditional logics, for which new, simpler, calculi are obtained.

The article Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies by Mark Kaminski, Sigurd Schneider and Gert Smolka gives a terminating tableau calculus for graded hybrid logic with global modalities, reflexivity, transitivity and role hierarchies. Termination of the system is achieved through pattern-based blocking, instead of the more common chain-based blocking. This approach leads to a NExpTime complexity bound for the decision procedure.

A wide range of logics is covered by the article Automated Synthesis of Tableau Calculi by Renate A. Schmidt and Dmitry Tishkovsky. It presents a method for synthesising sound and complete tableau calculi from a specification of the formal semantics of a logic. If the logic can be shown to admit finite filtration with respect to a well-defined first-order semantics then adding a general blocking mechanism provides a terminating tableau calculus.

The article On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics by Rajeev Goré, Linda Postniece and Alwen F. Tiu studies two kinds of deductive systems for tense logics: display calculi and deep inference calculi. Both are presented in a sequent calculus style. The paper shows that, for a range of extensions of tense logic, the two styles of calculi are equivalent, and there is a natural proof theoretic correspondence between display postulates and deep inference.

The issue concludes with the article Towards a Proof Theory of Gödel Modal Logics by George Metcalfe and Nicola Olivetti. It introduces analytic proof calculi for box and diamond fragments of basic modal fuzzy logics that combine the Kripke semantics of modal logic K with the many-valued semantics of Gödel logic. The calculi are used to establish completeness and complexity results for these fragments.

We would like to thank the authors for their excellent contributions, the anonymous reviewers for their thorough work, and the managing and executive editors of LMCS for their help and guidance throughout the preparation of this special issue.

Martin Giese and Arild Waaler
Guest Editors

1. Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis

Silvio Ghilardi ; Silvio Ranise.

The safety of infinite state systems can be checked by a backward reachability procedure. For certain classes of systems, it is possible to prove the termination of the procedure and hence conclude the decidability of the safety problem. Although backward reachability is property-directed, it can unnecessarily explore (large) portions of the state space of a system which are not required to verify the safety property under consideration. To avoid this, invariants can be used to dramatically prune the search space. Indeed, the problem is to guess such appropriate invariants. In this paper, we present a fully declarative and symbolic approach to the mechanization of backward reachability of infinite state systems manipulating arrays by Satisfiability Modulo Theories solving. Theories are used to specify the topology and the data manipulated by the system. We identify sufficient conditions on the theories to ensure the termination of backward reachability and we show the completeness of a method for invariant synthesis (obtained as the dual of backward reachability), again, under suitable hypotheses on the theories. We also present a pragmatic approach to interleave invariant synthesis and backward reachability so that a fix-point for the set of backward reachable states is more easily obtained. Finally, we discuss heuristics that allow us to derive an implementation of the techniques in the model checker MCMT, showing remarkable speed-ups on a significant set of safety problems […]

2. On Constructive Connectives and Systems

Arnon Avron ; Ori Lahav.

Canonical inference rules and canonical systems are defined in the framework of non-strict single-conclusion sequent systems, in which the succeedents of sequents can be empty. Important properties of this framework are investigated, and a general non-deterministic Kripke-style semantics is provided. This general semantics is then used to provide a constructive (and very natural), sufficient and necessary coherence criterion for the validity of the strong cut-elimination theorem in such a system. These results suggest new syntactic and semantic characterizations of basic constructive connectives.

3. Generic Modal Cut Elimination Applied to Conditional Logics

Dirk Pattinson ; Lutz Schröder.

We develop a general criterion for cut elimination in sequent calculi for propositional modal logics, which rests on absorption of cut, contraction, weakening and inversion by the purely modal part of the rule system. Our criterion applies also to a wide variety of logics outside the realm of normal modal logic. We give extensive example instantiations of our framework to various conditional logics. For these, we obtain fully internalised calculi which are substantially simpler than those known in the literature, along with leaner proofs of cut elimination and complexity. In one case, conditional logic with modus ponens and conditional excluded middle, cut elimination and complexity were explicitly stated as open in the literature.

4. Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies

Mark Kaminski ; Sigurd Schneider ; Gert Smolka.

We present a terminating tableau calculus for graded hybrid logic with global modalities, reflexivity, transitivity and role hierarchies. Termination of the system is achieved through pattern-based blocking. Previous approaches to related logics all rely on chain-based blocking. Besides being conceptually simple and suitable for efficient implementation, the pattern-based approach gives us a NExpTime complexity bound for the decision procedure.

5. Automated Synthesis of Tableau Calculi

Renate A. Schmidt ; Dmitry Tishkovsky.

This paper presents a method for synthesising sound and complete tableau calculi. Given a specification of the formal semantics of a logic, the method generates a set of tableau inference rules that can then be used to reason within the logic. The method guarantees that the generated rules form a calculus which is sound and constructively complete. If the logic can be shown to admit finite filtration with respect to a well-defined first-order semantics then adding a general blocking mechanism provides a terminating tableau calculus. The process of generating tableau rules can be completely automated and produces, together with the blocking mechanism, an automated procedure for generating tableau decision procedures. For illustration we show the workability of the approach for a description logic with transitive roles and propositional intuitionistic logic.

6. On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics

Rajeev Gore ; Linda Postniece ; Alwen F Tiu.

We consider two styles of proof calculi for a family of tense logics, presented in a formalism based on nested sequents. A nested sequent can be seen as a tree of traditional single-sided sequents. Our first style of calculi is what we call "shallow calculi", where inference rules are only applied at the root node in a nested sequent. Our shallow calculi are extensions of Kashima's calculus for tense logic and share an essential characteristic with display calculi, namely, the presence of structural rules called "display postulates". Shallow calculi enjoy a simple cut elimination procedure, but are unsuitable for proof search due to the presence of display postulates and other structural rules. The second style of calculi uses deep-inference, whereby inference rules can be applied at any node in a nested sequent. We show that, for a range of extensions of tense logic, the two styles of calculi are equivalent, and there is a natural proof theoretic correspondence between display postulates and deep inference. The deep inference calculi enjoy the subformula property and have no display postulates or other structural rules, making them a better framework for proof search.

7. Towards a Proof Theory of Gödel Modal Logics

George Metcalfe ; Nicola Olivetti.

Analytic proof calculi are introduced for box and diamond fragments of basic modal fuzzy logics that combine the Kripke semantics of modal logic K with the many-valued semantics of Gödel logic. The calculi are used to establish completeness and complexity results for these fragments.