: Wolfgang Bibel and Peter H. Schmitt, editors.
Automated Deduction. A basis for applications. Kluwer Academic Publishers, 1998. [ bib ]
: Peter Baumgartner, Ulrich Furbach, Michael Kohlhase, William McCune, Wolfgang Reif, Mark Stickel, and Tomàs Uribe, editors.
CADE-15 Workshop on Problem-solving Methodologies with Automated Deduction, 1998.
http://www.uni-koblenz.de/peter/cade-15-ws/. [ bib ]
: Harry de Swaart, editor.
Automated Reasoning with Analytic Tableaux and Related Methods, volume 1397 of Lecture Notes in Artificial Intelligence. Springer, 1998. [ bib ]
: Peter Baumgartner and Dorothea Schäfer.
Model Elimination with Simplification and its Application to Software Verification.
In Peter Baumgartner, Ulrich Furbach, Michael Kohlhase, William McCune, Wolfgang Reif, Mark Stickel, and Tomàs Uribe, editors, CADE-15 Workshop on Problem-solving Methodologies with Automated Deduction, 1998.
http://www.uni-koblenz.de/peter/cade-15-ws/. [ bib ]
: Peter Baumgartner and Ulrich Furbach.
Chapter I.3: Variants of Clausal Tableaux.
In Bibel and Schmitt [1], pages 73--102. [ bib ]
: Peter Baumgartner and Uwe Petermann.
Chapter II.6: Theory Reasoning.
In Bibel and Schmitt [1], pages 191--224. [ bib ]
: Peter Baumgartner.
Theory Reasoning in Connection Calculi, volume 1527 of Lecture Notes in Artificial Intelligence.
Springer, 1998. [ bib | .ps ]
: Peter Baumgartner.
Hyper Tableaux --- The Next Generation.
In de Swaart [3], pages 60--76. [ bib | .ps.gz ]
“Hyper tableaux” is a sound and complete calculus for first-order clausal logic. The present paper introduces an improvement which removes the major weakness of the calculus, which is the need to (at least partially) blindly guess ground-instantiations for certain clauses. This guessing is now replaced by a unification-driven technique.
The calculus is presented in detail, which includes a completeness proof. Completeness is proven by using a novel approach to extract a model from an open branch. This enables semantical redundancy criteria which are not present in related approaches.
: Peter Baumgartner, Ingo Dahn, Jürgen Dix, Ulrich Furbach, Micha Kühn, Frieder Stolzenburg, and Bernd Thomas.
Automated Deduction: A Technological Point of View.
KI, 12(4):7--14, 1998. [ bib | .pdf ]