Abstract is missing.
- Witness Runs for Counter Machines - (Abstract)Clark Barrett, Stéphane Demri, Morgan Deters. 1-4 [doi]
- On the Duality of Proofs and Countermodels in Labelled Sequent CalculiSara Negri. 5-9 [doi]
- A Brief Survey of Verified Decision Procedures for Equivalence of Regular ExpressionsTobias Nipkow, Maximilian Haslbeck. 10-12 [doi]
- Dealing with Symmetries in Modal TableauxCarlos Areces, Ezequiel Orbe. 13-27 [doi]
- Tableaux for Verification of Data-Centric ProcessesAndreas Bauer 0002, Peter Baumgartner, Martin Diller, Michael Norrish. 28-43 [doi]
- Bounded Proofs and Step FramesNick Bezhanishvili, Silvio Ghilardi. 44-58 [doi]
- Compression of Propositional Resolution Proofs by Lowering SubproofsJoseph Boudou, Bruno Woltzenlogel Paleo. 59-73 [doi]
- A Tableau System for Right Propositional Neighborhood Logic over Finite Linear Orders: An ImplementationDavide Bresolin, Dario Della Monica, Angelo Montanari, Guido Sciavicco. 74-80 [doi]
- Hypersequent and Labelled Calculi for Intermediate LogicsAgata Ciabattoni, Paolo Maffezioli, Lara Spendier. 81-96 [doi]
- TATL: Implementation of ATL Tableau-Based Decision ProcedureAmélie David. 97-103 [doi]
- A Terminating Evaluation-Driven Variant of G3iMauro Ferrari, Camillo Fiorentini, Guido Fiorino. 104-118 [doi]
- Model Checking General Linear Temporal LogicTim French, John Christopher McCabe-Dansted, Mark Reynolds. 119-133 [doi]
- Semantically Guided Evolution of ABoxesUlrich Furbach, Claudia Schon. 134-148 [doi]
- Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style ArchitectureStéphane Graham-Lengrand. 149-156 [doi]
- Understanding Resolution Proofs through Herbrand's TheoremStefan Hetzl, Tomer Libal, Martin Riener, Mikheil Rukhaia. 157-171 [doi]
- A Labelled Sequent Calculus for BBI: Proof Theory and Proof SearchZhe Hou, Alwen Tiu, Rajeev Goré. 172-187 [doi]
- A Refined Tableau Calculus with Controlled Blocking for the Description LogicMohammad Khodadadi, Renate A. Schmidt, Dmitry Tishkovsky. 188-202 [doi]
- Prefixed Tableau Systems for Logic of Proofs and ProvabilityHidenori Kurokawa. 203-218 [doi]
- Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5Björn Lellmann, Dirk Pattinson. 219-233 [doi]
- Schemata of Formulæ in the Theory of ArraysNicolas Peltier. 234-249 [doi]
- TAFA - A Tool for Admissibility in Finite AlgebrasChristoph Röthlisberger. 250-256 [doi]
- Formalizing Cut Elimination of Coalgebraic Logics in CoqHendrik Tews. 257-272 [doi]
- Intelligent Tableau Algorithm for DL ReasoningMing Zuo, Volker Haarslev. 273-287 [doi]