A transfinite knuth–bendix order for lambda-free higher-order terms

Heiko Becker, Jasmin Christian Blanchette*, Uwe Waldmann, Daniel Wand

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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.

Original languageEnglish
Title of host publicationAutomated Deduction - CADE 26
Subtitle of host publication26th International Conference on Automated Deduction, Proceedings
EditorsLeonardo de Moura
PublisherSpringer/Verlag
Pages432-453
Number of pages22
ISBN (Electronic)9783319630465
ISBN (Print)9783319630458
DOIs
Publication statusPublished - 2017
Event26th International Conference on Automated Deduction, CADE-26 2017 - Gothenburg, Sweden
Duration: 6 Aug 201711 Aug 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10395 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference26th International Conference on Automated Deduction, CADE-26 2017
CountrySweden
CityGothenburg
Period6/08/1711/08/17

Fingerprint Dive into the research topics of 'A transfinite knuth–bendix order for lambda-free higher-order terms'. Together they form a unique fingerprint.

  • Cite this

    Becker, H., Blanchette, J. C., Waldmann, U., & Wand, D. (2017). A transfinite knuth–bendix order for lambda-free higher-order terms. In L. de Moura (Ed.), Automated Deduction - CADE 26: 26th International Conference on Automated Deduction, Proceedings (pp. 432-453). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10395 LNAI). Springer/Verlag. https://doi.org/10.1007/978-3-319-63046-5_27