Automated Reasoning with Analytic Tableaux and Related Methods: 16th International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007. Proceedings

Piero A. Bonatti (auth.), Nicola Olivetti (eds.)3540730982, 9783540730989

This book constitutes the refereed proceedings of the 16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2007, held in Aix en Provence, France in July 2007.

The 14 revised research papers presented together with two system descriptions as well as three invited talks were carefully reviewed and selected from 43 submissions. The papers cover many topics in the wide range of logics, from intuitionistic and substructural logics to modal logics (including temporal and dynamic logics), from many-valued logics to nonmonotonic logics, and from classical first-order logic to description logics. Some contributions are focused on decision procedures, others on efficient reasoning, as well as on implementation of theorem provers. A few papers explore applications such as model-checking, verification, or knowledge engineering. In addition, other contributions make use of tableaux as a tool for theoretical investigation of logics.

---

Table of contents :
Front Matter….Pages –
Nonmonotonic Description Logics – Requirements, Theory, and Implementations….Pages 1-1
Our Quest for the Holy Grail of Agent Verification….Pages 2-9
An Abstract Framework for Satisfiability Modulo Theories….Pages 10-10
Axiom Pinpointing in General Tableaux….Pages 11-27
Proof Theory for First Order Łukasiewicz Logic….Pages 28-42
A Tableau Method for Public Announcement Logics….Pages 43-59
Bounded Model Checking with Description Logic Reasoning….Pages 60-72
Tableau Systems for Logics of Subinterval Structures over Dense Orderings….Pages 73-89
A Cut-Free Sequent Calculus for Bi-intuitionistic Logic….Pages 90-106
Tableaux with Dynamic Filtration for Layered Modal Logics….Pages 107-118
The Neighbourhood of S0.9 and S1….Pages 119-132
EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies….Pages 133-148
Tree-Sequent Methods for Subintuitionistic Predicate Logics….Pages 149-164
A Sequent Calculus for Bilattice-Based Logic and Its Many-Sorted Representation….Pages 165-182
Updating Reduced Implicate Tries….Pages 183-198
A Bottom-Up Approach to Clausal Tableaux….Pages 199-215
Differential Dynamic Logic for Verifying Parametric Hybrid Systems….Pages 216-232
Improvements to the Tableau Prover PITP….Pages 233-237
KLMLean 2.0: A Theorem Prover for KLM Logics of Nonmonotonic Reasoning….Pages 238-244
Back Matter….Pages –