Linear and Unit-Resulting Refutations for Horn Theories

Author: Baumgartner P.

Source: Journal of Automated Reasoning, Volume 16, Number 3, June 1996 , pp. 241-319(79)

Publisher: Springer

Buy & download fulltext article:

Price: $47.00 plus tax (Refund Policy)

Abstract:

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.

\parindent=1.5em 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.

Keywords: completion; linear resolution; unit-resulting resolution

Language: English

Document Type: Regular paper

Affiliations: 1: University of Koblenz, Institute for Computer Science, Rheinau 1, 56075 Koblenz, Germany e-mail: peter@informatik.uni-koblenz.de

Publication date: 1996-06-01