| 2013 | A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions. Tobias Nipkow, Maximilian P. L. Haslbeck |
| 2013 | A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search. Zhe Hou, Alwen Tiu, Rajeev Goré |
| 2013 | A Refined Tableau Calculus with Controlled Blocking for the Description Logic. Mohammad Khodadadi, Renate A. Schmidt, Dmitry Tishkovsky |
| 2013 | A Tableau System for Right Propositional Neighborhood Logic over Finite Linear Orders: An Implementation. Davide Bresolin, Dario Della Monica, Angelo Montanari, Guido Sciavicco |
| 2013 | A Terminating Evaluation-Driven Variant of G3i. Mauro Ferrari, Camillo Fiorentini, Guido Fiorino |
| 2013 | Automated Reasoning with Analytic Tableaux and Related Methods - 22th International Conference, TABLEAUX 2013, Nancy, France, September 16-19, 2013. Proceedings Didier Galmiche, Dominique Larchey-Wendling |
| 2013 | Bounded Proofs and Step Frames. Nick Bezhanishvili, Silvio Ghilardi |
| 2013 | Compression of Propositional Resolution Proofs by Lowering Subproofs. Joseph Boudou, Bruno Woltzenlogel Paleo |
| 2013 | Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5. Björn Lellmann, Dirk Pattinson |
| 2013 | Dealing with Symmetries in Modal Tableaux. Carlos Areces, Ezequiel Orbe |
| 2013 | Formalizing Cut Elimination of Coalgebraic Logics in Coq. Hendrik Tews |
| 2013 | Hypersequent and Labelled Calculi for Intermediate Logics. Agata Ciabattoni, Paolo Maffezioli, Lara Spendier |
| 2013 | Intelligent Tableau Algorithm for DL Reasoning. Ming Zuo, Volker Haarslev |
| 2013 | Model Checking General Linear Temporal Logic. Tim French, John Christopher McCabe-Dansted, Mark Reynolds |
| 2013 | On the Duality of Proofs and Countermodels in Labelled Sequent Calculi. Sara Negri |
| 2013 | Prefixed Tableau Systems for Logic of Proofs and Provability. Hidenori Kurokawa |
| 2013 | Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture. Stéphane Graham-Lengrand |
| 2013 | Schemata of Formulæ in the Theory of Arrays. Nicolas Peltier |
| 2013 | Semantically Guided Evolution of ABoxes. Ulrich Furbach, Claudia Schon |
| 2013 | TAFA - A Tool for Admissibility in Finite Algebras. Christoph Röthlisberger |
| 2013 | TATL: Implementation of ATL Tableau-Based Decision Procedure. Amélie David |
| 2013 | Tableaux for Verification of Data-Centric Processes. Andreas Bauer, Peter Baumgartner, Martin Diller, Michael Norrish |
| 2013 | Understanding Resolution Proofs through Herbrand's Theorem. Stefan Hetzl, Tomer Libal, Martin Riener, Mikheil Rukhaia |
| 2013 | Witness Runs for Counter Machines - (Abstract). Clark W. Barrett, Stéphane Demri, Morgan Deters |