Proving termination for term rewriting systems

Abstract

In the first part this paper gives an order-theoretic analysis of the multiset ordering, the recursive path ordering and the lexicographic path ordering with respect to order types and maximal order types. In the second part relativized ordinal notation systems, i. e. “ordinary” ordinal notation systems relativized to a given partial order, are introduced and investigated for the general study of precedence-based termination orderings. It is indicated that (at least) the reduction orderings mentioned above are special cases of this construction.