| 2015 | A Propositional Tableaux Based Proof Calculus for Reasoning with Default Rules. | Valentin Cassano, Carlos Gustavo Lpez Pombo, Thomas Stephen Edward Maibaum |
| 2015 | Integrating Simplex with Tableaux. | Guillaume Bury, David Delahaye |
| 2015 | A Dynamic Logic with Traces and Coinduction. | Richard Bubel, Crystal Chang Din, Reiner Hhnle, Keiko Nakata |
| 2015 | Disproving Inductive Entailments in Separation Logic via Base Pair Approximation. | James Brotherston, Nikos Gorogiannis |
| 2015 | Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations. | Taus Brock-Nannestad, Kaustuv Chaudhuri |
| 2015 | Realization Theorems for Justification Logics: Full Modularity. | Annemarie Borg, Roman Kuznets |
| 2015 | Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics. | Christoph Benzmller |
| 2015 | Efficient Algorithms for Bounded Rigid E-unification. | Peter Backeman, Philipp Rmmer |
| 2013 | Intelligent Tableau Algorithm for DL Reasoning. | Ming Zuo, Volker Haarslev |
| 2013 | Formalizing Cut Elimination of Coalgebraic Logics in Coq. | Hendrik Tews |
| 2013 | TAFA - A Tool for Admissibility in Finite Algebras. | Christoph Rthlisberger |
| 2013 | Schemata of Formul in the Theory of Arrays. | Nicolas Peltier |
| 2013 | A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions. | Tobias Nipkow, Maximilian P. L. Haslbeck |
| 2013 | On the Duality of Proofs and Countermodels in Labelled Sequent Calculi. | Sara Negri |
| 2013 | Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5. | Bjrn Lellmann, Dirk Pattinson |
| 2013 | Prefixed Tableau Systems for Logic of Proofs and Provability. | Hidenori Kurokawa |
| 2013 | A Refined Tableau Calculus with Controlled Blocking for the Description Logic. | Mohammad Khodadadi, Renate A. Schmidt, Dmitry Tishkovsky |
| 2013 | A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search. | Zhe Hou, Alwen Tiu, Rajeev Gor |
| 2013 | Understanding Resolution Proofs through Herbrand's Theorem. | Stefan Hetzl, Tomer Libal, Martin Riener, Mikheil Rukhaia |
| 2013 | Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture. | Stphane Graham-Lengrand |
| 2013 | Semantically Guided Evolution of ABoxes. | Ulrich Furbach, Claudia Schon |
| 2013 | Model Checking General Linear Temporal Logic. | Tim French, John Christopher McCabe-Dansted, Mark Reynolds |
| 2013 | A Terminating Evaluation-Driven Variant of G3i. | Mauro Ferrari, Camillo Fiorentini, Guido Fiorino |
| 2013 | TATL: Implementation of ATL Tableau-Based Decision Procedure. | Amlie David |
| 2013 | Hypersequent and Labelled Calculi for Intermediate Logics. | Agata Ciabattoni, Paolo Maffezioli, Lara Spendier |