Automated Reasoning with Analytic Tableaux and Related Methods

Presenting Constraints.- On the Use of Automata for Deciding Linear Arithmetic.- Comparative Concept Similarity over Minspaces: Axiomatisation and Tableaux Calculus.- A Schemata Calculus for Propositional Logic.- Tableaux and Model Checking for Memory Logics.- Canonical Constructive Systems.- A Novel Architecture for Situation Awareness Systems.- On the Proof Theory of Regular Fixed Points.- Decidability for Priorean Linear Time Using a Fixed-Point Labelled Calculus.- A Tableau-Based System for Spatial Reasoning about Directional Relations.- Terminating Tableaux for the Basic Fragment of Simple Type Theory.- Modular Sequent Systems for Modal Logic.- Abduction and Consequence Generation in a Support System for the Design of Logical Multiple-Choice Questions.- Goal-Directed Invariant Synthesis for Model Checking Modulo Theories.- Taming Displayed Tense Logics Using Nested Sequents with Deep Inference.- Sound Global State Caching for ALC with Inverse Roles.- A Tableau System for the Modal ?-Calculus.- Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies.- Prime Implicate Tries.- Proof Systems for a Gödel Modal Logic.- Generic Modal Cut Elimination Applied to Conditional Logics.- Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents.- Automated Synthesis of Tableau Calculi.- Tableaux for Projection Computation and Knowledge Compilation.