Paramodulation with non-monotonic orderings
Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio · 2003
All current completeness results for ordered paramodulation require the term ordering > to be well-founded, monotonic and total(izable) on ground terms. Here we introduce a new proof technique where the only properties required for > are well foundedness and the subterm property: The technique is a relatively simple and elegant application of some fundamental results on the termination and confluence of ground term rewrite systems (TRS). By a careful further analysis of our technique, we obtain the first Knuth-Bendix completion procedure that finds a convergent TRS for a given set of equations E and a (possibly non-totalizable) reduction ordering p whenever it exists. Note that being a reduction ordering is the minimal possible requirement on >, since a TRS terminates if, and only if, it is contained in a reduction ordering.