Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX 2000 St Andrews, Scotland, UK, July 3-7, 2000 Proceedings (Lecture Notes in Computer Science, 1847)

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. 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 - Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 3-7, 2000 Proceedings Author: Roy Dyckhoff Published by Springer Berlin Heidelberg ISBN: 978-3-540-67697-3 DOI: 10.1007/10722086 Table of Contents: Tableau Algorithms for Description Logics Modality and Databases Local Symmetries in Propositional Logic Design and Results of TANCS-2000 Non-classical (Modal) Systems Comparison Consistency Testing: The RACE Experience Benchmark Analysis with FaCT MSPASS: Modal Reasoning by Translation and First-Order Resolution TANCS-2000 Results for DLP Evaluating *SAT on TANCS 2000 Benchmarks A Labelled Tableau Calculus for Nonmonotonic (Cumulative) Consequence Relations A Tableau System for Gödel-Dummett Logic Based on a Hypersequent Calculus An Analytic Calculus for Quantified Propositional Gödel Logic A Tableau Method for Inconsistency-Adaptive Logics A Tableau Calculus for Integrating First-Order and Elementary Set Theory Reasoning Hypertableau and Path-Hypertableau Calculi for some Families of Intermediate Logics Variants of First-Order Modal Logics Complexity of Simple Dependent Bimodal Logics Properties of Embeddings from Int to S4 Term-Modal Logics A Subset-Matching Size-Bounded Cache for Satisfiability in Modal Logics

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.

This text constitutes the refereed proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2000. Topics covered range from theoretical foundations to implementation, systems development and applications.