Paramodulation and Knuth-Bendix completion with nontotal and nonmonotonic orderings
Up to now, all existing completeness results for ordered paramodulation and Knuth-Bendix completion have required term ordering > to be well founded, monotonic, and total( izable) on ground terms. For several applications, these requirements are too strong, and hence weakening them has been a well-known research challenge. Here we introduce a new completeness proof technique for ordered paramodulation where the only properties required on > 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 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.
term rewriting automated deduction