Two kinds of orderings are widely used in term rewriting and theorem proving, namely recursive path ordering (RPO) and Knuth-Bendix ordering (KBO). They provide powerful tools to prove the termination of rewriting systems. They are also applied in ordered resolution to prune the search space without compromising refutational completeness. Solving ordering constraints is therefore essential to the successful application of ordered rewriting and ordered resolution. Besides the needs for decision procedures for quantifier-free theories, situations arise in constrained deduction where the truth value of quantified formulae must be decided. Unfortunately, the full first-order theory of recursive path orderings is undecidable. This leaves an open question whether the first-order theory of KBO is decidable. In this paper, we give a positive answer to this question using quantifier elimination. In fact we shall show the decidability of a theory that is more expressive than the theory of KBO.
In Proc. of the 20th International Conference on Automated Deduction (CADE'05), Tallinn, Estonia, July 2005, Springer Verlag, LNCS 3632, pp 131-148.
BibTex, Postscript, PDF. © 2005, Springer Verlag.
Long version (including proofs): Postscript, PDF.