Paramodulation with Well-founded Orderings.

Saved in:

Bibliographic Details
Title:	Paramodulation with Well-founded Orderings.
Authors:	BOFILL, MIQUEL¹ mbofill@ima.udg.edu, RUBIO, ALBERT² rubio@lsi.upc.edu
Source:	Journal of Logic & Computation. Apr2009, Vol. 19 Issue 2, p263-302. 40p.
Subjects:	Rewriting systems (Computer science), Equations, Proof theory, Monotonic functions, Completeness theorem, Mathematical logic
Abstract:	For many years, all existing completeness results for Knuth-Bendix completion and ordered paramodulation required the term ordering ¿ to be well-founded, monotonic and total(izable) on ground terms. Then, it was shown that well-foundedness and the subterm property were enough for ensuring completeness of ordered paramodulation. Here we show that the subterm property is not necessary either. By using a new restricted form of rewriting, we obtain a completeness proof of ordered paramodulation for Horn clauses with equality, where well-foundedness of the ordering suffices. Apart from the theoretical significance of this result, some potential applications motivating the interest of dropping the subterm property are given. The proof of the results included in this article, being still technical in some parts, is pretty much shorter and easier to read than the one we have in the preliminary version of this work presented at the CADE, 2002 conference (Bofill, and Rubio, 2002, CADE, Vol. 2392 of LNAI, pp. 456-470). [ABSTRACT FROM AUTHOR]
	Copyright of Journal of Logic & Computation is the property of Oxford University Press / USA and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database:	Engineering Source

Description
Abstract:	For many years, all existing completeness results for Knuth-Bendix completion and ordered paramodulation required the term ordering ¿ to be well-founded, monotonic and total(izable) on ground terms. Then, it was shown that well-foundedness and the subterm property were enough for ensuring completeness of ordered paramodulation. Here we show that the subterm property is not necessary either. By using a new restricted form of rewriting, we obtain a completeness proof of ordered paramodulation for Horn clauses with equality, where well-foundedness of the ordering suffices. Apart from the theoretical significance of this result, some potential applications motivating the interest of dropping the subterm property are given. The proof of the results included in this article, being still technical in some parts, is pretty much shorter and easier to read than the one we have in the preliminary version of this work presented at the CADE, 2002 conference (Bofill, and Rubio, 2002, CADE, Vol. 2392 of LNAI, pp. 456-470). [ABSTRACT FROM AUTHOR]
ISSN:	0955792X