Decomposition ordering at a tool to prove the termination of rewriting systems
Pierre Lescanne · International Joint Conference on Artificial Intelligence · 1981
Decomposition ordering is a well-founded monotonic ordering on terms. Because it has the subterm and the deletion properties, decomposition ordering is useful to prove termination of rewriting systems. An algorithm comparing two terms is given.