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
T2 - 26th International Conference on Automated Deduction, CADE-26 2017
Y2 - 6 August 2017 through 11 August 2017
ER -