Order-sorted Term Rewriting
A. J. J. Dick · The Computer Journal · 1991
In this article we look at the motivation for order-sorted term rewriting by considering some of the very natural equational theories in which single-sorted (unsorted) and many-sorted rewriting lack sufficient expressiveness, for various reasons. However, order-sorted rewriting is not without problems of its own, and we consider some of these along with a brief description in each case of some current approaches to their solution.