Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX 2002 Copenhagen, Denmark, July 30 – August 1, 2002 Proceedings

Matthias Baaz (auth.), Uwe Egly, Chritian G. Fermüller (eds.)3540439293, 9783540439295

This book constitutes the refereed proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2002, held in Copenhagen, Denmark, in July/August 2002.
The 20 revised full papers and two system descriptions presented together with two invited contributions were carefully reviewed and selected for inclusion in the book. All current issues surrounding the mechanization of logical reasoning with tableaux and similar methods are addressed. Among the logic calculi investigated are linear logic, temporal logic, modal logics, hybrid logic, multi-modal logics, fuzzy logics, Goedel logic, Lukasiewicz logic, intermediate logics, quantified boolean logic, and, of course, classical first-order logic.

---

Table of contents :
Proof Analysis by Resolution….Pages 1-1
Using Linear Logic to Reason about Sequent Systems….Pages 2-23
A Schütte-Tait Style Cut-Elimination Proof for First-Order Gödel Logic….Pages 24-37
Tableaux for Quantified Hybrid Logic….Pages 38-52
Tableau-Based Automated Deduction for Duration Calculus….Pages 53-69
Linear Time Logic, Conditioned Models, and Planning with Incomplete Knowledge….Pages 70-84
A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic….Pages 85-99
Modal Nonmonotonic Logics Revisited: Efficient Encodings for the Basic Reasoning Tasks….Pages 100-114
Tableau Calculi for the Logics of Finite k -Ary Trees….Pages 115-129
A Model Generation Style Completeness Proof for Constraint Tableaux with Superposition….Pages 130-144
Implementation and Optimisation of a Tableau Algorithm for the Guarded Fragment….Pages 145-159
Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas….Pages 160-175
Integration of Equality Reasoning into the Disconnection Calculus….Pages 176-190
Analytic Sequent Calculi for Abelian and Łukasiewicz Logics….Pages 191-205
Analytic Tableau Systems for Propositional Bimodal Logics of Knowledge and Belief….Pages 206-220
A Confluent Theory Connection Calculus….Pages 221-234
On Uniform Word Problems Involving Bridging Operators on Distributive Lattices….Pages 235-250
Question Answering: From Partitions to Prolog….Pages 251-265
A General Theorem Prover for Quantified Modal Logics….Pages 266-280
Some New Exceptions for the Semantic Tableaux Version of the Second Incompleteness Theorem….Pages 281-297
A New Indefinite Semantics for Hilbert’s Epsilon….Pages 298-314
A Tableau Calculus for Combining Non-disjoint Theories….Pages 315-329
LINK: A Proof Environment Based on Proof Nets….Pages 330-334
DCTP 1.2 — System Abstract….Pages 335-339