Abstract

We study the complexity of term rewrite systems compatible with the Knuth–Bendix order, if the signature of the rewrite system is potentially infinite. We show that the known bounds on the derivation height are essentially preserved, if the rewrite system fulfils some mild conditions. This allows us to obtain bounds on the derivational height of non-simply terminating rewrite systems. As a corollary, we re-establish an essentially optimal 2-recursive upper bound on the derivational complexity of finite rewrite systems compatible with a Knuth–Bendix order. Furthermore, we link our main result to results on generalized Knuth–Bendix orders and to recent results on transfinite Knuth–Bendix orders.

BibTeX

@Article{M:2014,
  author = 	 {Georg Moser},
  title = 	 {KBOs, Ordinals, Subrecursive Hierarchies and All That},
  journal = 	 {Journal of Logic and Computations},
  year = 	 {2014},
  doi = {10.1093/logcom/exu072}
  note = 	 {advance access},
}