Solving Knuth-Bendix Ordering Constraints

Konstantin Korovin

Solving ordering constrains is used in automated deduction to prune the search space. Mainly two kinds of orders are used; the Knuth-Bendix orders and recursive path orders. For recursive path orders, decidability of constraint solving was shown by Comon, and NP-completeness by Nieuwenhuis. We show that for the Knuth-Bendix order the constraint solvability problem is NP-complete. For constraints consisting of a single inequality we present a polynomial time algorithm. More information can be found at http://www.cs.man.ac.uk/~korovink.