Abstract. We generalize the various path orderings and the conditions under which they work, and describe an implementation of this general ordering. We look at methods for proving...
Usually termination of term rewriting systems TRS's is proved by means of a monotonic well-founded order. If this order is total on ground terms, the TRS is called totally ...
We propose an extension of rewriting techniques to derive inclusion relations a ⊆ b between terms built from monotonic operators. Instead of using only a rewriting relation ⊆ â...