Name
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 firstorder theorem provers and describe relationships between the transfinite Knuth-Bendix orders and existing implementations of extensions of the Knuth-Bendix orders. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-22438-6_29 | CADE |
Keywords | Field | DocType |
subterm coefficient,general case ordinal,finite subterm coefficient,finite signature,transfinite knuth-bendix order,firstorder theorem provers,finite sequence,natural number,fixed length,knuth-bendix order | Theorem provers,Discrete mathematics,Natural number,Ordinal number,Transfinite number,Mathematics | Conference |
Volume | ISSN | Citations |
6803 | 0302-9743 | 6 |
PageRank | References | Authors |
0.52 | 16 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Laura Kovács | 1 | 494 | 36.97 |
| Georg Moser | 2 | 196 | 15.29 |
| Andrei Voronkov | 3 | 2670 | 225.46 |