A new decision procedure for the existential fragment of ordering constraints expressed using the recursive path ordering is presented. This procedure is nondeterministic and checks whether a set of constraints is solvable over the given signature, i.e., the signature over which the terms in the constraints are defined. It is shown that this non-deterministic procedure runs in polynomial time, thus establishing the membership of this problem in the complexity class NP for the first time.
CITATION STYLE
Narendran, P., Rusinowitch, M., & Verma, R. (1999). RPO constraint solving is in NP. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1584, pp. 385–398). Springer Verlag. https://doi.org/10.1007/10703163_26
Mendeley helps you to discover research relevant for your work.