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

Heiko Becker; Jasmin Christian Blanchette; Uwe Waldmann; Daniel Wand

doi:10.1007/978-3-319-63046-5_27

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 proceeding › Conference contribution › Academic › peer-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 language	English
Title of host publication	Automated Deduction - CADE 26
Subtitle of host publication	26th International Conference on Automated Deduction, Proceedings
Editors	Leonardo de Moura
Publisher	Springer/Verlag
Pages	432-453
Number of pages	22
ISBN (Electronic)	9783319630465
ISBN (Print)	9783319630458
DOIs	https://doi.org/10.1007/978-3-319-63046-5_27
Publication status	Published - 2017
Event	26th International Conference on Automated Deduction, CADE-26 2017 - Gothenburg, Sweden Duration: 6 Aug 2017 → 11 Aug 2017

Publication series

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

Conference

Conference	26th International Conference on Automated Deduction, CADE-26 2017
Country	Sweden
City	Gothenburg
Period	6/08/17 → 11/08/17

Access to Document

10.1007/978-3-319-63046-5_27

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

Becker, Heiko ; Blanchette, Jasmin Christian ; Waldmann, Uwe ; Wand, Daniel. / A transfinite knuth–bendix order for lambda-free higher-order terms. Automated Deduction - CADE 26: 26th International Conference on Automated Deduction, Proceedings. editor / Leonardo de Moura. Springer/Verlag, 2017. pp. 432-453 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{fdecf8ec932f42ef8d0d2c980e8c4934,

title = "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.",

author = "Heiko Becker and Blanchette, {Jasmin Christian} and Uwe Waldmann and Daniel Wand",

year = "2017",

doi = "10.1007/978-3-319-63046-5_27",

language = "English",

isbn = "9783319630458",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer/Verlag",

pages = "432--453",

editor = "{de Moura}, Leonardo",

booktitle = "Automated Deduction - CADE 26",

}

Becker, H, Blanchette, JC, 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10395 LNAI, Springer/Verlag, pp. 432-453, 26th International Conference on Automated Deduction, CADE-26 2017, Gothenburg, Sweden, 6/08/17. https://doi.org/10.1007/978-3-319-63046-5_27

A transfinite knuth–bendix order for lambda-free higher-order terms. / Becker, Heiko; Blanchette, Jasmin Christian; Waldmann, Uwe; Wand, Daniel.

Automated Deduction - CADE 26: 26th International Conference on Automated Deduction, Proceedings. ed. / Leonardo de Moura. Springer/Verlag, 2017. p. 432-453 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10395 LNAI).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - Becker, Heiko

AU - Blanchette, Jasmin Christian

AU - Waldmann, Uwe

AU - Wand, Daniel

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85026772769&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85026772769&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-63046-5_27

DO - 10.1007/978-3-319-63046-5_27

M3 - Conference contribution

AN - SCOPUS:85026772769

SN - 9783319630458

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 432

EP - 453

BT - Automated Deduction - CADE 26

A2 - de Moura, Leonardo

PB - Springer/Verlag

ER -

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