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 条

[21] HIGHER-ORDER CURVATURE TERMS AND EXTENDED INFLATION
WANG, Y
PHYSICAL REVIEW D, 1990, 42 (08): : 2541 - 2547
[22] HIGHER-ORDER HYPERFINE TERMS IN SPIN HAMILTONIAN
GOLDING, RM
STUBBS, LC
PROCEEDINGS OF THE ROYAL SOCIETY OF LONDON SERIES A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES, 1978, 362 (1711): : 525 - 536
[23] PHASES OF HIGHER-ORDER TERMS IN THE TOPOLOGICAL EXPANSION
JONES, CE
USCHERSOHN, J
PHYSICAL REVIEW D, 1985, 32 (10): : 2698 - 2706
[24] Umbrella integration with higher-order correction terms
Kaestner, Johannes
JOURNAL OF CHEMICAL PHYSICS, 2012, 136 (23):
[25] Higher-Order Intentionality and Higher-Order Acquaintance
Benj Hellie
Philosophical Studies, 2007, 134 : 289 - 324
[26] Higher-Order Kerr Terms Allow Ionization-Free Filamentation in Gases
Bejot, P.
Kasparian, J.
Henin, S.
Loriot, V.
Vieillard, T.
Hertz, E.
Faucher, O.
Lavorel, B.
Wolf, J. -P.
PHYSICAL REVIEW LETTERS, 2010, 104 (10)
[27] Higher-order intentionality and higher-order acquaintance
Hellie, Benj
PHILOSOPHICAL STUDIES, 2007, 134 (03) : 289 - 324
[28] The recursive path and polynomial ordering for first-order and higher-order terms
Bofill, Miquel
Borralleras, Cristina
Rodriguez-Carbonell, Enric
Rubio, Albert
JOURNAL OF LOGIC AND COMPUTATION, 2013, 23 (01) : 263 - 305
[29] MATRIX MODEL PERTURBED BY HIGHER-ORDER CURVATURE TERMS
KORCHEMSKY, GP
MODERN PHYSICS LETTERS A, 1992, 7 (33) : 3081 - 3100
[30] RECURSIVE GENERATION OF HIGHER-ORDER TERMS IN THE MAGNUS EXPANSION
KLARSFELD, S
OTEO, JA
PHYSICAL REVIEW A, 1989, 39 (07): : 3270 - 3273

← 1 2 3 4 5 →