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.