On the Complexity of Simplification Orderings
Joachim Peter Steinbach · 1993
Various methods for proving the termination of term rewriting systems have been suggested. Most of them are based on the notion of simplification ordering. In this paper, the theoretical time complexities (of the worst cases) of a collection of well-known simplification orderings will be presented. 1 Introduction and Summary Term rewriting systems (TRSs, for short) provide a powerful tool for expressing nondeterministic computations and as a result they have been widely used as, for example, in theorem provers. Moreover, they can usefully be applied in many other areas of computer science and mathematics such as abstract data type specifications and program verification. A main requirement of TRSs is expressed by the termination property. There exist various methods of proving the termination of TRSs. Most of these are based on reduction orderings which are well-founded, compatible with the structure of terms 1 and stable with respect to (w.r.t., for short) substitutions. The notion...