Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX’98 Oisterwijk, The Netherlands, May 5–8, 1998 Proceedings

N. G. de Bruijn (auth.), Harrie de Swart (eds.)3540644067, 9783540644064

This book constitutes the refereed proceedings of the 1998 International Conference on Analytic Tableaux and Related Methods, TABLEAUX’98, held in Oisterwijk near Tilburg, The Netherlands, in May 1998. The volume presents 17 revised full papers and three system descriptions selected from 34 submissions; also included are several abstracts of invited lectures, tutorials, and system comparison papers. The book presents new research results for automated deduction in various non-standard logics as well as in classical logic. Areas of application include software verification, systems verification, deductive databases, knowledge representation and its required inference engines, and system diagnosis.

---

Table of contents :
Philosophical Aspects of Computerized Verification of Mathematics….Pages 1-9
A Science of Reasoning (Extended Abstract)….Pages 10-17
Model Checking: Historical Perspective and Example (Extended Abstract)….Pages 18-24
Comparison of Theorem Provers for Modal Logics — Introduction and Summary….Pages 25-26
FaCT and DLP….Pages 27-30
Prover KT4….Pages 31-32
leanK 2.0….Pages 33-34
Logics Workbench 1.0….Pages 35-35
Optimised Functional Translation and Resolution….Pages 36-37
Benchmark Evaluation of □KE….Pages 38-39
Implementation of Propositional Temporal Logics Using BDDs….Pages 40-41
Computer Programming as Mathematics in a Programming Language and Proof System CL….Pages 42-43
A Tableau Calculus for Multimodal Logics and Some (Un)Decidability Results….Pages 44-59
Hyper Tableau — The Next Generation….Pages 60-76
Fibring Semantic Tableaux….Pages 77-92
A Tableau Calculus for Quantifier-Free Set Theoretic Formulae….Pages 93-107
A Tableau Method for Interval Temporal Logic with Projection….Pages 108-123
Bounded Model Search in Linear Temporal Logic and Its Application to Planning….Pages 124-140
On Proof Complexity of Circumscription….Pages 141-155
Tableaux for Finite-Valued Logics with Arbitrary Distribution Modalities….Pages 156-171
Some Remarks on Completeness, Connection Graph Resolution, and Link Deletion….Pages 172-186
Simplification and Backjumping in Modal Tableau….Pages 187-201
Free Variable Tableaux for a Logic with Term Declarations….Pages 202-216
Simplification A General Constraint Propagation Technique for Propositional and Modal Tableaux….Pages 217-231
A Tableaux Calculus for Ambiguous Quantifiation….Pages 232-246
From Kripke Models to Algebraic Counter-Valuations….Pages 247-261
Deleting Redundancy in Proof Reconstruction….Pages 262-276
A New One-Pass Tableau Calculus for PLTL ….Pages 277-291
Decision Procedures for Intuitionistic Propositional Logic by Program Extraction….Pages 292-306
The FaCT System….Pages 307-312
Implementation of Proof Search in the Imperative Programming Language Pizza….Pages 313-319
p-SETHEO: Strategy Parallelism in Automated Theorem Proving….Pages 320-324