On recursive path ordering (Q1082075): Difference between revisions

The ''recursive path ordering'' (RPO) scheme of Dershowitz is a powerful way of extending a partial order on a set of function symbols to a well- founded partial order on their set of terms. We prove that, given a pair of terms, the problem of deciding whether they can be made RPO- comparable, by choosing a partial order on their function symbols, is NP- complete.