A new ordering constraint solving method and its applications
Robert Nieuwenhuis · MPG.PuRe (Max Planck Society) · 1992
We show that it is possible to transform any given LPO ordering constraint $C$ into a finite equivalent set of constraints $S$ for which a special kind of solutions can be obtained. This allows to compute the equalities that follow from ordering constraints, and to decide e.g.\\ whether an {\\em ordering constrained equation\\/} is a tautology. Another application we develop here is a method to check ordered rewrite systems for (ground) confluence.