Linear and Unit-Resulting Refutations for Horn Theories
Author: Baumgartner P.1
Source: Journal of Automated Reasoning, Volume 16, Number 3, June 1996 , pp. 241-319(79)
Publisher: Springer
- Free Content
- New Content
- Subscribed Content
- Free Trial Content
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
- Free Content
- New Content
- Subscribed Content
- Free Trial Content
Click here for Page Help