[Zurück]


Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):

L. Kovacs, G. Moser, A. Voronkov:
"On Transfinite Knuth-Bendix Orders";
Vortrag: 23rd International Conference on Automated Deduction (CADE-23), Wroclaw, Poland; 31.07.2011 - 05.08.2011; in: "Proc. of the 23rd International Conference on Automated Deduction (CADE-23)", N. Bjorner, V. Sofronie-Stokkermans (Hrg.); Springer, LNAI 6803 (2011), ISBN: 978-3-642-22437-9; S. 384 - 399.



Kurzfassung deutsch:
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 \omega^\omega,
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.

Kurzfassung englisch:
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 \omega^\omega,
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.

Schlagworte:
term rewriting, ordinals, theorem proving, KBO


Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/PubDat_205735.pdf


Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.