Paramodulation with Well-founded Orderings
Miquel Bofill, Albert Rubio · Journal of Logic and Computation · 2008
Abstract For many years, all existing completeness results for Knuth-Bendix completion and ordered paramodulation required the term order-ing ≻ 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 us-ing 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 signifi-cance of this result, some potential applications motivating the interest of dropping the subterm property are given. The proof of the results included in this paper, 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 [8]. Key words: term rewriting, equational reasoning, theorem proving, paramodulation, Knuth-Bendix completion 1