This book constitutes the refereed proceedings of the 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009, held in Oslo, Norway, in July 2009.
The 21 revised research papers presented together with 1 system description and 2 invited talks were carefully reviewed and selected from 44 submissions. The papers cover many topics in the wide range of applications of tableaux and related methods in areas such as hardware and software verfications, semantic technologies, and knowledge engineering.
Author(s): Peter Jeavons (auth.), Martin Giese, Arild Waaler (eds.)
Series: Lecture Notes in Computer Science 5607 : Lecture Notes in Artificial Intelligence
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2009
Language: English
Pages: 341
Tags: Artificial Intelligence (incl. Robotics); Mathematical Logic and Formal Languages; Programming Techniques; Software Engineering
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 -
