Derivation lengths and order types of Knuth-Bendix orders

Abstract

The derivation length function of a finite term rewriting system terminating via a Knuth-Bendix order is shown to be bounded by the Ackermann function applied to a single exponential function. This result is essentially optimal as there are rewrite systems with such derivation lengths. In a second part the order types of Knuth-Bendix orders over finite signatures are classified within the ordinals up to ωω. © 2001 Elsevier Science B.V. All rights reserved.