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

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