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

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 formulas 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.

• Type: Conference
• Year: 2005
• Where: CADE
• Authors: Ting Zhang, Henny B. Sipma, Zohar Manna
• Keywords: Automated Reasoning, CADE 2005, First-order Theory, Recursive Path, Recursive Path Orderings