A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms

Abstract : We generalize the Knuth-Bendix order (KBO) to higher-order terms without λ-abstraction. The restriction of this new order to first-order terms coincides with the traditional KBO. The order has many useful properties, including transitivity, the subterm property, compatibility with contexts (monotonicity), stability under substitution, and well-foundedness. Transfinite weights and argument coefficients can also be supported. The order appears promising as the basis of a higher-order superposition calculus.
Document type :
Conference papers
Complete list of metadatas

Cited literature [50 references]  Display  Hide  Download

https://hal.inria.fr/hal-01592186
Contributor : Stephan Merz <>
Submitted on : Wednesday, September 27, 2017 - 6:48:24 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:04 PM
Long-term archiving on : Thursday, December 28, 2017 - 12:40:00 PM

File

BeckerBlanchetteWaldmannWandCA...
Files produced by the author(s)

Identifiers

Collections

Citation

Heiko Becker, Jasmin Blanchette, Uwe Waldmann, Daniel Wand. A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. CADE-26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. pp.432-453, ⟨10.1007/978-3-319-63046-5_27⟩. ⟨hal-01592186⟩

Share

Metrics

Record views

203

Files downloads

81