Automated Reasoning with Analytic Tableaux and Related Methods

- Invited Talks

- Witness Runs for Counter Machines (Abstract)

- On the Duality of Proofs and Countermodels in Labelled Sequent Calculi

- A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions

- Research Papers

- Dealing with Symmetries in Modal Tableaux

- Tableaux for Verification of Data-Centric Processes

- Bounded Proofs and Step Frames

- Compression of Propositional Resolution Proofs by Lowering Subproofs

- A Tableau System for Right Propositional Neighborhood Logic over Finite Linear Orders: An Implementation

- Hypersequent and Labelled Calculi for Intermediate Logics

- TATL: Implementation of ATL Tableau-Based Decision Procedure

- A Terminating Evaluation-Driven Variant of G3i

- Model Checking General Linear Temporal Logic

- Semantically Guided Evolution of SHI ABoxes

- Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture

- Understanding Resolution Proofs through Herbrand's Theorem

- A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search

- A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI

- Prefixed Tableau Systems for Logic of Proofs and Provability

- Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5

- Schemata of Formulæ in the Theory of Arrays

- TAFA - A Tool for Admissibility in Finite Algebras

- Formalizing Cut Elimination of Coalgebraic Logics in Coq

- Intelligent Tableau Algorithm for DL Reasoning