Abstract

In this paper we discuss the recently introduced transfinite Knuth-Bendix orders. We prove
that any such order with finite subterm coefficients and for a finite signature is equivalent
to an order using ordinals below ω^ω, that is, finite sequences of natural numbers of a fixed
length. We show that this result does not hold when subterm coefficients are infinite. However,
we prove that in this general case ordinals below ω^ω^ω suffice. We also prove that both
upper bounds are tight. We briefly discuss the significance of our results for the implementation
of first-order theorem provers and describe relationships between the transfinite Knuth-Bendix
orders and existing implementations of extensions of the Knuth-Bendix orders.

BibTeX

@inproceedings{LKGMAV-CADE11,
  author    = "Laura Kov\'{a}cs and Georg Moser and Andrei Voronkov",
  title     = "On Transfinite Knuth-Bendix Orders",
  booktitle = "Proceedings of the 23rd International Conference on
               Automated Deduction",
  address   = "Wroclaw",
  series    = "Lecture Notes in Artificial Intelligence",
  volume    = 6803,
  pages     = "384--399",
  year      = 2011
}