Termination of term rewriting by interpretation
Hans Zantema · TU/e Research Portal · 1992
We investigate how to prove termination of term rewriting systems by interpretation of terms. This can be considered as a generalization of polynomial interpretations. A classification of types of termination is proposed built on properties in the semantic level. A transformation on term rewriting systems eliminating distributive rules is introduced. Using this distribution elimination a new termination proof of SUBST from [9] is given.