ABSTRACT

All the properties of reduction systems described in Section 7.2 can be applied to term rewriting systems. Given a term rewriting system R, we have to find an equivalent complete terminating rewriting system. In this section we assume that our system is terminating. The termination of term rewriting systems will be considered in the next section. As we did in the example given in Section 7.2, we proceed by transforming critical pairs into new reduction rules.