The following submission have been accepted for inclusion in the Tableaux 2013 program and conference proceedings. They appear in their submission order.


  1. Tim French, John Mccabe-Dansted and Mark Reynolds. Model Checking for Compositional Models of General Linear Time.
  2. Agata Ciabattoni, Paolo Maffezioli and Lara Spendier. Hypersequent and Labelled Calculi for Intermediate Logics.
  3. Nick Bezhanishvili and Silvio Ghilardi. Bounded proofs and step frames.
  4. Amélie David. TATL: Implementation of an ATL Tableau-Based Decision Procedure.
  5. Zhe Hou, Alwen Tiu and Rajeev Gore. A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search.
  6. Ming Zuo and Volker Haarslev. Intelligent Tableaux Algorithm for DL Reasoning.
  7. Nicolas Peltier. Schemata of formulae in the theory of arrays.
  8. Stefan Hetzl, Tomer Libal, Martin Riener and Mikheil Rukhaia. Understanding Resolution Proofs through Herbrand's Theorem.
  9. Hendrik Tews. Formalizing Cut Elimination of Coalgebraic Logics in Coq.
  10. Bruno Woltzenlogel Paleo and Joseph Boudou. Compression of Propositional Resolution Proofs by Lowering Subproofs.
  11. Andreas Bauer, Peter Baumgartner, Martin Diller and Michael Norrish. Tableaux for Verification of Data-Centric Processes.
  12. Bjoern Lellmann and Dirk Pattinson. Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5.
  13. Claudia Schon and Ulrich Furbach. Semantically Guided Evolution of SHI ABoxes.
  14. Carlos Areces and Ezequiel Orbe. Dealing with Symmetries in Modal Tableaux.
  15. Mauro Ferrari, Camillo Fiorentini and Guido Fiorino. A terminating evaluation-driven variant of G3i.
  16. Mohammad Khodadadi, Renate A. Schmidt and Dmitry Tishkovsky. A Refined Tableau calculus with Controlled Blocking for the Description Logic SHOI.
  17. Christoph Röthlisberger. TAFA - A Tool for Admissibility in Finite Algebras.
  18. Hidenori Kurokawa. Prefixed tableau systems for logic of proofs and provability.
  19. Davide Bresolin, Dario Della Monica, Angelo Montanari and Guido Sciavicco. A Tableau System for Right Propositional Neighborhood Logic over Finite Linear Orders: an Implementation (System Description).
  20. Stéphane Graham-Lengrand. Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture.