Simple LPO constraint solving methods (Q685481)

Satisfiability of lexicographic path ordering constraints was shown to be decidable under the given signature by \textit{H. Comon} [Int. J. Found. Comp. Sci. 1, No. 4, 387-411 (1990; Zbl 0722.03012)]; the author and \textit{A. Rubio} [Theorem proving with ordering constrained clauses, Proc. 11th Int. Conf. on Automated Deduction, Saratoga Springs, NY, Springer, Berlin, 477-491 (1992)] obtained the like result for satisfiability under extended signatures. Both satisfiability problem are now proved to be NP- complete by reducing the constraints to disjunctions of ``simple systems'' (conjunctions of equalities and inequalities); it is argued that this technique should have practical relevance.