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 formulas must be decided. Unfortunately, the full first-order theory of lexicographic path ordering (LPO), the most popular form of RPO, 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.

Download