Several kinds of orderings, such as polynomial orderings, lexicographic path
orderings and Knuth-Bendix orderings, are widely used in term rewriting and
theorem proving. In term rewriting, these orderings are powerful tools in
proving termination of rewriting systems. In theorem proving, they are key
instruments to prune 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 existential theories, situations arise
in constrained deduction where the satisfiability of arbitrarily quantified
formulas need be decided. Unfortunately, the first-order theory of
lexicographic path orderings is undecidable, so is existential theory of
polynomial orderings. This leaves an open question whether the first-order
theory of Knuth-Bendix orderings is decidable (RTA problem 99). In this
talk, we give a positive answer to this question using quantifier
elimination on a complex structure containing term algebras and integer
arithmetic. In fact, we shall show the decidability of a theory that is more
expressive than the theory of Knuth-Bendix orderings.