## The Decidability of the First-order Theory of Knuth-Bendix Order

Ting Zhang,
Henny Sipma,
Zohar Manna.
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.

© Henny Sipma /
sipma@cs.stanford.edu
Last modified: Nov 19 14:40:50 PDT 2004