2011 | OriginalPaper | Chapter
On Transfinite Knuth-Bendix Orders
Authors : Laura Kovács, Georg Moser, Andrei Voronkov
Published in: Automated Deduction – CADE-23
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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
$\omega^{\omega^{\omega}}$
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.