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

Ting Zhang, Henny B. Sipma, Zohar Manna



Abstract


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 (RTA open problem #99). 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.

Download


Proceeding Version (CADE-20)
Conference Talk (CADE-20)
Journal Version