For many years all known 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 fundamental interest of this result, some potential applications motivating the interest of dropping the subterm property
are given.
Both authors partially supported by the spanish CICYT project MAVERISH ref. TIC2001-2476-C03-01, M. Bofill is also supported
by the spanish CICYT project CADVIAL ref. TIC2001-2392-C03-01 and A. Rubio is also supported by the spanish DURSI group 2001SGR
00254.