On a monotonic semantic path ordering
Alfons Geser · OPen Access Repositorium der Universität Ulm (OPARU) (Ulm University) · 1992
The semantic path ordering preceq_spo is an ordering that allows to prove termination of term rewriting systems. Unlike other such orderings, it is not monotonic. We construct two monotonic suborderings preceq_cspo, preceq_mspo, of preceq_spo. Both orderings rely on reasonable assumptions on the underlying semantic ordering, and mirror Kamin/L"evy"s termination proof method. Moreover, preceq_mspo is shown to cover preceq_spo up to the subterm property. In the case of the semantic ordering being a simplification quasiordering, the three orderings even coincide. Thus the Knuth/Bendix ordering turns out to be a special case of the semantic path ordering.