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.