Automated Reasoning with Analytic Tableaux and Related Methods: 18th International Conference, TABLEAUX 2009, Oslo, Norway, July 6-10, 2009. Proceedings

Front Matter....Pages -
Presenting Constraints....Pages 1-15
On the Use of Automata for Deciding Linear Arithmetic....Pages 16-16
Comparative Concept Similarity over Minspaces: Axiomatisation and Tableaux Calculus....Pages 17-31
A Schemata Calculus for Propositional Logic....Pages 32-46
Tableaux and Model Checking for Memory Logics....Pages 47-61
Canonical Constructive Systems....Pages 62-76
A Novel Architecture for Situation Awareness Systems....Pages 77-92
On the Proof Theory of Regular Fixed Points....Pages 93-107
Decidability for Priorean Linear Time Using a Fixed-Point Labelled Calculus....Pages 108-122
A Tableau-Based System for Spatial Reasoning about Directional Relations....Pages 123-137
Terminating Tableaux for the Basic Fragment of Simple Type Theory....Pages 138-151
Modular Sequent Systems for Modal Logic....Pages 152-166
Abduction and Consequence Generation in a Support System for the Design of Logical Multiple-Choice Questions....Pages 167-172
Goal-Directed Invariant Synthesis for Model Checking Modulo Theories....Pages 173-188
Taming Displayed Tense Logics Using Nested Sequents with Deep Inference....Pages 189-204
Sound Global State Caching for ALC with Inverse Roles....Pages 205-219
A Tableau System for the Modal μ -Calculus....Pages 220-234
Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies....Pages 235-249
Prime Implicate Tries....Pages 250-264
Proof Systems for a Gödel Modal Logic....Pages 265-279
Generic Modal Cut Elimination Applied to Conditional Logics....Pages 280-294
Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents....Pages 295-309
Automated Synthesis of Tableau Calculi....Pages 310-324
Tableaux for Projection Computation and Knowledge Compilation....Pages 325-340
Back Matter....Pages -