Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 3-7, 2000 Proceedings

Franz Baader, Ulrike Sattler (auth.), Roy Dyckhoff (eds.)354067697X, 9783540676973

This book constitutes the refereed proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2000, held in St Andrews, Scotland, UK, in July 2000.
The 23 revised full papers and 2 system descriptions presented were carefully reviewed and selected from 42 submissions. Also included are 3 invited lectures and 6 nonclassical system comparisons. All current issues surrounding the mechanization of reasoning with tableaux and similar methods are addressed – ranging from theoretical foundations to implementation, systems development, and applications, as well as covering a broad variety of logical calculi.

---

Table of contents :
Front Matter….Pages –
Tableau Algorithms for Description Logics….Pages 1-18
Modality and Databases….Pages 19-39
Local Symmetries in Propositional Logic….Pages 40-51
Design and Results of TANCS-2000 Non-classical (Modal) Systems Comparison….Pages 52-56
Consistency Testing: The RACE Experience….Pages 57-61
Benchmark Analysis with FaCT….Pages 62-66
MSPASS: Modal Reasoning by Translation and First-Order Resolution….Pages 67-71
TANCS-2000 Results for DLP….Pages 72-76
Evaluating *SAT on TANCS 2000 Benchmarks….Pages 77-81
A Labelled Tableau Calculus for Nonmonotonic (Cumulative) Consequence Relations….Pages 82-97
A Tableau System for Gödel-Dummett Logic Based on a Hypersequent Calculus….Pages 98-111
An Analytic Calculus for Quantified Propositional Gödel Logic….Pages 112-126
A Tableau Method for Inconsistency-Adaptive Logics….Pages 127-142
A Tableau Calculus for Integrating First-Order and Elementary Set Theory Reasoning….Pages 143-159
Hypertableau and Path-Hypertableau Calculi for some Families of Intermediate Logics….Pages 160-174
Variants of First-Order Modal Logics….Pages 175-189
Complexity of Simple Dependent Bimodal Logics….Pages 190-204
Properties of Embeddings from Int to S4 ….Pages 205-219
Term-Modal Logics….Pages 220-236
A Subset-Matching Size-Bounded Cache for Satisfiability in Modal Logics….Pages 237-251
Dual Intuitionistic Logic Revisited….Pages 252-267
Model Sets in a Nonconstructive Logic of Partial Terms with Definite Descriptions….Pages 268-278
Search Space Compression in Connection Tableau Calculi Using Disjunctive Constraints….Pages 279-293
Matrix-Based Inductive Theorem Proving….Pages 294-308
Monotonic Preorders for Free Variable Tableaux….Pages 309-323
The Mosaic Method for Temporal Logics….Pages 324-340
Sequent-Like Tableau Systems with the Analytic Superformula Property for the Modal Logics KB , KDB , K5 , KD5 ….Pages 341-351
A Tableau Calculus for Equilibrium Entailment….Pages 352-367
Towards Tableau-Based Decision Procedures for Non-Well-Founded Fragments of Set Theory….Pages 368-382
Tableau Calculus for Only Knowing and Knowing At Most….Pages 383-397
A Tableau-Like Representation Framework for Efficient Proof Reconstruction….Pages 398-414
The Semantic Tableaux Version of the Second Incompleteness Theorem Extends Almost to Robinson’s Arithmetic Q….Pages 415-430
Redundancy-Free Lemmatization in the Automated Model-Elimination Theorem Prover AI-SETHEO….Pages 431-435
E-SETHEO: An Automated 3 Theorem Prover….Pages 436-440
Back Matter….Pages –