Automated Reasoning with Analytic Tableaux and Related Methods: 22nd International Conference, TABLEAUX 2013, Nancy, France, September 16-19, 2013, Proceedings

Front Matter....Pages -
Witness Runs for Counter Machines....Pages 1-4
On the Duality of Proofs and Countermodels in Labelled Sequent Calculi....Pages 5-9
A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions....Pages 10-12
Dealing with Symmetries in Modal Tableaux....Pages 13-27
Tableaux for Verification of Data-Centric Processes....Pages 28-43
Bounded Proofs and Step Frames....Pages 44-58
Compression of Propositional Resolution Proofs by Lowering Subproofs....Pages 59-73
A Tableau System for Right Propositional Neighborhood Logic over Finite Linear Orders: An Implementation....Pages 74-80
Hypersequent and Labelled Calculi for Intermediate Logics....Pages 81-96
TATL: Implementation of ATL Tableau-Based Decision Procedure....Pages 97-103
A Terminating Evaluation-Driven Variant of G3i....Pages 104-118
Model Checking General Linear Temporal Logic....Pages 119-133
Semantically Guided Evolution of $\\mathcal{SHI}$ ABoxes....Pages 134-148
 Psyche : A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture....Pages 149-156
Understanding Resolution Proofs through Herbrand’s Theorem....Pages 157-171
A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search....Pages 172-187
A Refined Tableau Calculus with Controlled Blocking for the Description Logic $\\mathcal{SHOI}$ ....Pages 188-202
Prefixed Tableau Systems for Logic of Proofs and Provability....Pages 203-218
Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5....Pages 219-233
Schemata of Formulæ in the Theory of Arrays....Pages 234-249
 TAFA – A Tool for Admissibility in Finite Algebras....Pages 250-256
Formalizing Cut Elimination of Coalgebraic Logics in Coq....Pages 257-272
Intelligent Tableau Algorithm for DL Reasoning....Pages 273-287
Back Matter....Pages -