On Transfinite Knuth-Bendix Orders

Laura Kovács, Georg Moser, and Andrei Voronkov

Proceedings of the 23rd International Conference on Automated Deduction (CADE 2011), Lecture Notes in Artificial Intelligence 6803, pp. 384 – 399, 2011.


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.


  PDF |    doi:10.1007/978-3-642-22438-6_29  |  © Springer


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
Nach oben scrollen