Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX’97 Pont-à -Mousson, France, May 13–16, 1997 Proceedings

Ryuzo Hasegawa, Hiroshi Fujita (auth.), Didier Galmiche (eds.)3540629203, 9783540629207

This book constitutes the refereed proceedings of the International Conference on Analytic Tableaux and Related Methods, TABLEAUX’97, held in Pont-a-Mousson, France, in May 1997.
The volume presents 22 revised full papers selected from a total of 49 submissions. Also included are two invited papers and two system descriptions. The volume covers the whole spectrum of tableaux-based theorem proving and its applications including theoretical foundations, methodological issues, implementation techniques, and system development. Besides classical logics, among the logics dealt with are modal, intuitionistic, many-valued, and temporal logic.

---

Table of contents :

Content:
Front Matter….Pages –
MGTP: A model generation theorem prover — Its advanced features and applications —….Pages 1-15
Three faces of natural deduction….Pages 16-30
Tableaux for logic programming with strong negation….Pages 31-42
Generalized tableau systems for intermediate propositional logics….Pages 43-61
Lean induction principles for tableaux….Pages 62-75
Tableaux for diagnosis applications….Pages 76-90
Free variable tableaux for propositional modal logics….Pages 91-106
A sequent calculus for skeptical Default Logic….Pages 107-121
A fast saturation strategy for set-theoretic tableaux….Pages 122-137
Hintikka multiplicities in matrix decision methods for some propositional modal logics….Pages 138-152
Automated natural deduction prover and experiments….Pages 153-157
Non-elementary speed-ups in proof length by different variants of classical analytic calculi….Pages 158-172
Ordered tableaux: Extensions and applications….Pages 173-187
Two loop detection mechanisms: A comparison….Pages 188-200
Subgoal alternation in model elimination….Pages 201-215
Projection: A unification procedure for tableaux in Conceptual Graphs….Pages 216-230
On quasitautologies….Pages 231-245
Tableaux methods for access control in distributed systems….Pages 246-260
Proving correctness of labeled transition systems by semantic tableaux….Pages 261-275
Tableau methods for PA-processes….Pages 276-290
A tableau proof system for a mazurkiewicz trace logic with fixpoints….Pages 291-306
ileanTAP: An intuitionistic theorem prover….Pages 307-312
Simplifying and generalizing formulae in tableaux. Pruning the search space and building models….Pages 313-327
A framework for using knowledge in tableau proofs….Pages 328-342
A sequent calculus for reasoning in four-valued Description Logics….Pages 343-357
Tableaux for functional dependencies and independencies….Pages 358-372
Back Matter….Pages –