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

被引：14
|
作者：
Becker, Heiko [1 ]
Blanchette, Jasmin Christian [2 ,3 ,4 ]
Waldmann, Uwe [4 ]
Wand, Daniel [4 ,5 ]
机构：
[1] Max Planck Inst Softwaresyst, Saarbrucken, Germany
[2] Vrije Univ Amsterdam, Amsterdam, Netherlands
[3] Inria Nancy Grand Est, Villers Les Nancy, France
[4] Max Planck Inst Informat, Saarbrucken, Germany
[5] Tech Univ Munich, Munich, Germany
来源：
AUTOMATED DEDUCTION - CADE 26 | 2017年 / 10395卷
基金：
欧洲研究理事会;
关键词：
TERMINATION; PATH; LOGIC;
D O I：
10.1007/978-3-319-63046-5_27
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We generalize the Knuth-Bendix order (KBO) to higher-order terms without lambda-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.
引用
收藏
页码：432 / 453
页数：22
相关论文
共 50 条
  • [1] A higher-order Knuth-Bendix procedure and its applications
    Kusakari, Keiichirou
    Chiba, Yuki
    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2007, E90D (04) : 707 - 715
  • [2] The Embedding Path Order for Lambda-Free Higher-Order Terms
    Bentkamp A.
    Journal of Applied Logics, 2021, 8 (10): : 2447 - 2470
  • [3] THE EMBEDDING PATH ORDER FOR LAMBDA-FREE HIGHER-ORDER TERMS
    Bentkamp, Alexander
    JOURNAL OF APPLIED LOGICS-IFCOLOG JOURNAL OF LOGICS AND THEIR APPLICATIONS, 2021, 8 (10): : 2447 - 2469
  • [4] On Transfinite Knuth-Bendix Orders
    Kovacs, Laura
    Moser, Georg
    Voronkov, Andrei
    AUTOMATED DEDUCTION - CADA-23, 2011, 6803 : 384 - +
  • [5] A Lambda-Free Higher-Order Recursive Path Order
    Blanchette, Jasmin Christian
    Waldmann, Uwe
    Wand, Daniel
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS 2017), 2017, 10203 : 461 - 479
  • [6] SUPERPOSITION FOR LAMBDA-FREE HIGHER-ORDER LOGIC
    Bentkamp, Alexander
    Blanchette, Jasmin
    Cruanes, Simon
    Waldmann, Uwe
    LOGICAL METHODS IN COMPUTER SCIENCE, 2021, 17 (02) : 1:1 - 1:38
  • [7] Superposition for Lambda-Free Higher-Order Logic
    Bentkamp, Alexander
    Blanchette, Jasmin Christian
    Cruanes, Simon
    Waldmann, Uwe
    AUTOMATED REASONING, IJCAR 2018, 2018, 10900 : 28 - 46
  • [8] Orienting equalities with the Knuth-Bendix order
    Korovin, K
    Voronkov, A
    18TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2003, : 75 - 84
  • [9] Orienting rewrite rules with the Knuth-Bendix order
    Korovin, K
    Voronkov, A
    INFORMATION AND COMPUTATION, 2003, 183 (02) : 165 - 186
  • [10] An AC-compatible Knuth-Bendix order
    Korovin, K
    Voronkov, A
    AUTOMATED DEDUCTION - CADE-19, PROCEEDINGS, 2003, 2741 : 47 - 59
12345