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

13 Downloads (Pure)

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, Gothenburg, Sweden, August 6–11, 2017, 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
Country/TerritorySweden
CityGothenburg
Period6/08/1711/08/17

Funding

We are grateful to Stephan Merz, Tobias Nipkow, and Christoph Weidenbach for making this research possible; to Mathias Fleury and Dmitriy Traytel for helping us formalize the syntactic ordinals; to Andrei Popescu and Christian Sternagel for advice with extending a partial well-founded order to a total one in the mechanized proof of Lemma 3; to Andrei Voronkov for the enlightening discussion about KBO at the IJCAR 2016 banquet; and to Carsten Fuhs, Mark Summerfield, and the anonymous reviewers for suggesting many textual improvements. Blanchette has received funding from the European Research Council (ERC) under the European Union?s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Wand is supported by the Deutsche Forschungsgemeinschaft (DFG) grant Hardening the Hammer (NI 491/14-1).

FundersFunder number
Horizon 2020 Framework Programme713999
European Research Council
Deutsche ForschungsgemeinschaftNI 491/14-1

    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