Theorem Proving with Analytic Tableaux and Related Methods: 5th International Workshop, TABLEAUX ’96 Terrasini, Palermo, Italy, May 15–17, 1996 Proceedings

Peter B. Andrews, Matthew Bishop (auth.), P. Miglioli, U. Moscato, D. Mundici, M. Ornaghi (eds.)3540612084, 9783540612087

This books presents the refereed proceedings of the Fifth International Workshop on Analytic Tableaux and Related Methods, TABLEAUX ’96, held in Terrasini near Palermo, Italy, in May 1996.
The 18 full revised papers included together with two invited papers present state-of-the-art results in this dynamic area of research. Besides more traditional aspects of tableaux reasoning, the collection also contains several papers dealing with other approaches to automated reasoning. The spectrum of logics dealt with covers several nonclassical logics, including modal, intuitionistic, many-valued, temporal and linear logic.

---

Table of contents :
On sets, types, fixed points, and checkerboards….Pages 1-15
Fibred tableaux for multi-implication logics….Pages 16-35
Interpolation for a sequent calculus of generalized quantifiers….Pages 36-47
Almost duplication-free tableau calculi for prepositional lax logics….Pages 48-64
Combining many-valued and intuitionistic tableaux….Pages 65-79
Cyclic connections….Pages 80-92
Incremental theory reasoning methods for semantic tableaux….Pages 93-109
The disconnection method….Pages 110-126
Sequent calculi for default and autoepistemic logics….Pages 127-142
Minimal model generation with positive unit hyper-resolution tableaux….Pages 143-159
Distributed modal theorem proving with KE….Pages 160-176
A simple tableau system for the logic of elsewhere….Pages 177-192
Situational Calculus, linear connection proofs and STRIPS-like planning: An experimental comparison….Pages 193-209
Efficient loop-check for backward proof search in some non-classical propositional logics….Pages 210-225
Strong normalization for all-style LK tq ….Pages 226-243
T-string unification: Unifying prefixes in non-classical proof methods….Pages 244-260
A timing refinement of intuitionistic proofs and its application to the timing analysis of combinational circuits….Pages 261-277
A tableau calculus for minimal model reasoning….Pages 278-294
On the intuitionistic force of classical search (Extended abstract)….Pages 295-311
Proof-search in intuitionistic logic based on constraint satisfaction….Pages 312-329