Comparing and putting together recursive path ordering, simplification orderings and Non-Ascending property for termination proofs of term rewriting systems

Abstract

We give a sufficient condition for proving strong termination in Combinatory Logic and Rewriting Systems which solves an open problem [Böh 77]. We also compare, in the context of general rewriting systems, the power of that condition and other known methods, as the recursive path orderings and simplification orderings, presenting original results. A new technique for proving strong termination, called Diagram of Matchings, is also introduced. In many cases it allows to combine together the strength of various methods of proof.