Automated Reasoning with Analytic Tableaux and Related Methods: 14th International Conference, TABLEAUX 2005, Koblenz, Germany, September 14-17, 2005. Proceedings

Diego Calvanese (auth.), Bernhard Beckert (eds.)3540289313, 9783540289319

This book constitutes the refereed proceedings of the 14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2005, held in Koblenz, Germany, in September 2005.

The 18 revised research papers presented together with 7 system descriptions as well as 4 invited talks were carefully reviewed and selected from 46 submissions. All aspects of the mechanization of reasoning with tableaux and related methods are focused: analytic tableaux for various logics, related techniques and concepts, new calculi and methods for theorem proving in classical and non-classical logics, systems, tools, and implementations. It puts a special emphasis on applications of tableaux and related methods in areas such as, for example, hardware and software verification, knowledge engineering, and semantic Web.

---

Table of contents :
Front Matter….Pages –
Query Processing in Peer-to-Peer Systems: An Epistemic Logic Approach….Pages 1-1
Description Logics in Ontology Applications….Pages 2-13
Automated Reasoning in the Context of the Semantic Web….Pages 14-14
Formal Versus Rigorous Mathematics: How to Get Your Papers Published….Pages 15-32
Consistency of Variable Splitting in Free Variable Systems of First-Order Logic….Pages 33-47
On the Dynamic Increase of Multiplicities in Matrix Proof Methods for Classical Higher-Order Logic….Pages 48-62
A Tableau-Based Decision Procedure for Right Propositional Neighborhood Logic….Pages 63-77
Cyclic Proofs for First-Order Logic with Inductive Definitions….Pages 78-92
A Tableau-Based Decision Procedure for a Fragment of Graph Theory Involving Reachability and Acyclicity….Pages 93-107
Embedding Static Analysis into Tableaux and Sequent Based Frameworks….Pages 108-122
A Calculus for Type Predicates and Type Coercion….Pages 123-137
A Tableau Calculus with Automaton-Labelled Formulae for Regular Grammar Logics….Pages 138-152
Comparing Instance Generation Methods for Automated Reasoning….Pages 153-168
An Order-Sorted Quantified Modal Logic for Meta-ontology….Pages 169-184
A Redundancy Analysis of Sequent Proofs….Pages 185-200
A Tableau Algorithm for Description Logics with Concrete Domains and GCIs….Pages 201-216
The Space Efficiency of OSHL….Pages 217-230
Efficient Query Processing with Compiled Knowledge Bases….Pages 231-244
Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic….Pages 245-261
Automatic ‘Descente Infinie’ Induction Reasoning….Pages 262-276
A Decision Procedure for the Alternation-Free Two-Way Modal μ -Calculus….Pages 277-291
On the Partial Respects in Which a Real Valued Arithmetic System Can Verify Its Tableaux Consistency….Pages 292-306
Pdk: The System and Its Language….Pages 307-311
Proof Output and Transformation for Disconnection Tableaux….Pages 312-317
LoTREC: Logical Tableaux Research Engineering Companion….Pages 318-322
A Tableau-Based Explainer for DL Subsumption….Pages 323-327
CondLean 3.0: Improving CondLean for Stronger Conditional Logics….Pages 328-332
The ILTP Library: Benchmarking Automated Theorem Provers for Intuitionistic Logic….Pages 333-337
Unit Propagation in a Tableau Framework….Pages 338-342
Back Matter….Pages –