Peter Baumgartner.
Linear and Unit-Resulting Refutations for Horn Theories.
Journal of Automated Reasoning, 16(3):241-319, June 1996. [ bib | .pdf ]
We present a new transformation method by which a given Horn theory is transformed in such a way that resolution derivations can be carried out which are both linear (in the sense of Prologs SLD-resolution) and unit-resulting (i.e. the resolvents are unit clauses). This is not trivial since although both strategies alone are complete, their naïve combination is not. Completeness is recovered by our method through a completion procedure in the spirit of Knuth-Bendix completion, however with different ordering criteria. A powerful redundancy criterion helps to find a finite system quite often.
The transformed theory can be used in combination with linear calculi such as e.g. (theory) model elimination to yield sound, complete and efficient calculi for full first order clause logic over the given Horn theory.
As an example application, our method discovers a generalization of the well-known linear paramodulation calculus for the combined theory of equality and strict orderings.
The method has been implemented and has been tested in conjunction with a model elimination theorem prover.

 
Peter Baumgartner, Jürgen Dix, Ulrich Furbach, Dorothea Schäfer, and Frieder Stolzenburg.
Deduktion und Logisches Programmieren.
KI, 10(2):34-39, 1996. [ bib ]
 
Peter Baumgartner, Ulrich Furbach, and Ilkka Niemelä.
Hyper Tableaux.
In Logics in Artificial Intelligence (JELIA '96), number 1126 in Lecture Notes in Artificial Intelligence. Springer, 1996. [ bib | .pdf ]
This paper introduces a variant of clausal normal form tableaux that we call “hyper tableaux”. Hyper tableaux keep many desirable features of analytic tableaux while taking advantage of the central idea from (positive) hyper resolution, namely to resolve away all negative literals of a clause in a single inference step. Another feature of the proposed calculus is the extensive use of universally quantified variables. This enables new efficient forward-chaining proof procedures for full first order theories as variants of tableaux calculi.

 
Peter Baumgartner.
Theory Reasoning in Connection Calculi and the Linearizing Completion Approach.
PhD thesis, Universität Koblenz-Landau, 1996. [ bib | .pdf ]
This thesis is on extensions of calculi for automated theorem proving towards theory reasoning. It focuses on connection methods and in particular on theory model elimination (TME). For TME the emphasis lies on the combination with theory reasoners to be obtained by new compilation approach.

Several theory-reasoning versions of connection calculi are defined and related to each other. In doing so, TME will be selected as a base to be developed further. The final versions are search-space restricted versions of total TME, partial TME and partial restart TME. These versions all are answer-complete, thus making TME interesting for logic programming and problem-solving applications.

A theory reasoning system is only operable in combination with an (efficient) background reasoner for the theories of interest. Instead of hand-crafting respective background reasoners, a more general approach - linearizing completion - is proposed. Linearizing completion enables the automatic construction of background calculi suitable for TME-based theory reasoning systems from a wide range of axiomatically given theories, namely Horn theories.

Technically, linearizing completion is a device for combining the unit-resulting strategy of resolution with a goal-oriented, linear strategy à la Prolog in a refutationally complete way. The method is presented in detail.

Finally, an implementation extending the PTTP technique (Prolog based Technology Theorem Proving) towards theory reasoning is described, and the usefulness of the methods developed in this text will be experimentally demonstrated.

 
Peter Baumgartner and Ulrich Furbach.
Hyper Tableaux. Part I: Proof Procedure and Model Generation.
Dagstuhl-Seminar Reports Disjunctive logic programming and databases: Non-monotonic aspects, 1996. [ bib ]
 
Peter Baumgartner and Ulrich Furbach.
Hyper Tableaux and Disjunctive Logic Programming.
In ICLP 96 Workshop on Deductive Databases and Logic Programming, volume 295 of GMD Studien. GMD, 1996. [ bib | .pdf ]
We introduce a bottom-up and a top-down calculus for disjunctive logic programming (DLP). The bottom-up calculus, hyper tableaux, is depicted in its ground version and its relation to fixed point approaches from the literature is investigated. The top-down calculus, restart model elimination (RME), is presented as a sound and complete answer-computing mechanism for DLPs, and its relation to hyper tableaux is discussed.
In two aspect this represents an extension of SLD-resolution for Horn clause logic programming: RME is SLD-resolution when restricted to Horn clauses, and it has a direct counterpart to the immediate consequence operator for Horn clauses. Furthermore we discuss, that hyper tableaux can be seen as an extension of SLO-resolution.

 
Artificial Intelligence Research Group.
Towards Merging Theorem Proving and Logic Programming Paradigms.
Proc. of the Poster Session at JICSLP '96, Editors: N. Fuchs and U. Geske, 1996.
GMD Studien Nr. 296. [ bib ]
 
Peter Baumgartner, Bernhard Beckert, and Michael Kühn.
Extending Hyper Tableaux with Rigid E-Unification.
In K. Prasser, editor, Workshop Deduktion, 20. Jahrestagung für künstliche Intelligenz, Zusammenfassungen, number WV-96-09 in Internal Reports, Fakultät Informatik, D01062 Dresden, 1996. Technische Universität Dresden. [ bib | .pdf ]
In [?] we introduced a variant of clausal normal form tableaux called “hyper tableaux”. In the talk we well report about ongoing work on two improvements of the basic calculus. The first improvement deals with a shortcoming of the basic calculus, which is the need for “purifying” substitutions in disjunctions of positive literals. The second improvement is the extension with a dedicated inference rule for equality. We will use the completion-based method for mixed universal and rigid E-unification of [?].