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 条
  • [31] HIGHER-ORDER TERMS IN THE DIELECTRIC CONSTANT OF IONIC CRYSTALS
    SZIGETI, B
    PROCEEDINGS OF THE ROYAL SOCIETY OF LONDON SERIES A-MATHEMATICAL AND PHYSICAL SCIENCES, 1959, 252 (1269): : 217 - 235
  • [32] HIGHER-ORDER TERMS IN THE ANISOTROPIC REPRESENTATION OF REYNOLDS STRESSES
    HORIUTI, K
    PHYSICS OF FLUIDS A-FLUID DYNAMICS, 1990, 2 (10): : 1708 - 1710
  • [33] Proving the Equivalence of Higher-Order Terms by Means of Supercompilation
    Klyuchnikov, Ilya
    Romanenko, Sergei
    PERSPECTIVES OF SYSTEMS INFORMATICS, 2010, 5947 : 193 - 205
  • [34] EXACT SUMMATION OF HIGHER-ORDER TERMS IN MULTIPHOTON PROCESSES
    GONTIER, Y
    RAHMAN, NK
    TRAHIN, M
    PHYSICAL REVIEW A, 1976, 14 (06): : 2109 - 2125
  • [35] Role of Higher-Order Terms in Local Piston Theory
    Meijer, Marius-Corne
    Dala, Laurent
    JOURNAL OF AIRCRAFT, 2019, 56 (01): : 388 - 391
  • [36] APPEARANCE OF HIGHER-ORDER TERMS IN THE LQ ISOEFFECT EQUATION
    SCHULTHEISS, TE
    ZAGARS, GK
    MEDICAL PHYSICS, 1986, 13 (04) : 614 - 614
  • [37] Oscillatory Behavior of Higher-Order DEs with Delay Terms
    Balatta, Shoura Ahmed
    Ismail, Eddie Shahril
    Hashim, Ishak
    Bataineh, Ahmad Sami
    Momani, Shaher
    EUROPEAN JOURNAL OF PURE AND APPLIED MATHEMATICS, 2023, 16 (04): : 2234 - 2246
  • [38] On the Effectiveness of Higher-Order Terms in Refined Beam Theories
    Carrera, Erasmo
    Petrolo, Marco
    JOURNAL OF APPLIED MECHANICS-TRANSACTIONS OF THE ASME, 2011, 78 (02):
  • [39] HIGHER-ORDER TERMS IN EPSILON EXPANSION OF POMERON PROPAGATOR
    BAKER, M
    PHYSICS LETTERS B, 1974, B 51 (02) : 158 - 160
  • [40] HIGHER-ORDER TERMS OF ASYMPTOTIC EXPANSIONS FOR SPHEROIDAL EIGENVALUES
    WANG, WX
    QUARTERLY OF APPLIED MATHEMATICS, 1989, 47 (03) : 539 - 543
12345