Sciweavers

Share
CADE
2005
Springer

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

10 years 8 months ago
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.
Ting Zhang, Henny B. Sipma, Zohar Manna
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2005
Where CADE
Authors Ting Zhang, Henny B. Sipma, Zohar Manna
Comments (0)
books