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.

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 [?].

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.

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.

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.