Theorem proving with analytic tableaux and related methods. 5th international workshop, TABLEAUX '96, Terrasini, Palermo, Italy, May 15--17, 1996. Proceedings (Q1913544)

The articles of this volume will be reviewed individually. The previous conference has been announced (see Zbl 0878.00080). Indexed articles: \textit{Andrews, Peter B.; Bishop, Matthew}, On sets, types, fixed points, and checkerboards, 1-15 [Zbl 1415.03012] \textit{D'Agostino, Marcello; Gabbay, Dov M.}, Fibred tableaux for multi-implication logics, 16-35 [Zbl 1415.03020] \textit{Alechina, Natasha}, Interpolation for a sequent calculus of generalized quantifiers, 36-47 [Zbl 1415.03043] \textit{Avellone, Alessandro; Ferrari, Mauro}, Almost duplication-free tableau calculi for propositional lax logics, 48-64 [Zbl 1415.03013] \textit{Baaz, Matthias; Fermüller, Christian G.}, Combining many-valued and intuitionistic tableaux, 65-79 [Zbl 1415.03016] \textit{Becher, Gérard}, Cyclic connections, 80-92 [Zbl 1415.03017] \textit{Beckert, Bernhard; Pape, Christian}, Incremental theory reasoning methods for semantic tableaux, 93-109 [Zbl 1412.68208] \textit{Billon, Jean-Paul}, The disconnection method, 110-126 [Zbl 1412.68210] \textit{Bonatti, Piero A.}, Sequent calculi for default and autoepistemic logics, 127-142 [Zbl 1415.03055] \textit{Bry, François; Yahya, Adnan}, Minimal model generation with positive unit hyper-resolution tableaux, 143-159 [Zbl 1412.68212] \textit{Pitt, Jeremy; Cunningham, Jim}, Distributed modal theorem proving with KE, 160-176 [Zbl 1412.68254] \textit{Demri, Stéphane}, A simple tableau system for the logic of elsewhere, 177-192 [Zbl 1415.03021] \textit{Fronhöfer, Bertram}, Situational calculus, linear connection proofs and STRIPS-like planning: an experimental comparison, 193-209 [Zbl 1412.68223] \textit{Heuerding, Alain; Seyfried, Michael; Zimmermann, Heinrich}, Efficient loop-check for backward proof search in some non-classical propositional logics, 210-225 [Zbl 1415.03023] \textit{Joinet, Jean-Baptiste; Schellinx, Harold; Tortora de Falco, Lorenzo}, Strong normalization for all-style \(\mathbf{LK}^\mathrm{tq}\), 226-243 [Zbl 1415.03056] \textit{Otten, Jens; Kreitz, Christoph}, T-string unification: unifying prefixes in non-classical proof methods, 244-260 [Zbl 1412.68251] \textit{Mendler, Michael}, A timing refinement of intuitionistic proofs and its application to the timing analysis of combinational circuits, 261-277 [Zbl 1412.68139] \textit{Niemelä, Ilkka}, A tableau calculus for minimal model reasoning, 278-294 [Zbl 1412.68247] \textit{Ritter, Eike; Pym, David; Wallen, Lincoln}, On the intuitionistic force of classical search (extended abstract), 295-311 [Zbl 1415.03028] \textit{Voronkov, Andrei}, Proof-search in intuitionistic logic based on constraint satisfaction, 312-329 [Zbl 1415.03010]