Talks and Poster Presentations (with Proceedings-Entry):
L. Kovacs, G. Moser, A. Voronkov:
"On Transfinite Knuth-Bendix Orders";
Talk: 23rd International Conference on Automated Deduction (CADE-23),
Wroclaw, Poland;
07-31-2011
- 08-05-2011; in: "Proc. of the 23rd International Conference on Automated Deduction (CADE-23)",
N. Bjorner, V. Sofronie-Stokkermans (ed.);
Springer,
LNAI 6803
(2011),
ISBN: 978-3-642-22437-9;
384
- 399.
English 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 \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.
German 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 \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.
Keywords:
term rewriting, ordinals, theorem proving, KBO
Electronic version of the publication:
http://publik.tuwien.ac.at/files/PubDat_205735.pdf
Created from the Publication Database of the Vienna University of Technology.