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 条

[11] The decidability of the first-order theory of Knuth-Bendix order
Zhang, T
Sipma, HB
Manna, Z
AUTOMATED DEDUCTION - CADE-20, PROCEEDINGS, 2005, 3632 : 131 - 148
[12] Extending a brainiac prover to lambda-free higher-order logic
Vukmirovic, Petar
Blanchette, Jasmin
Cruanes, Simon
Schulz, Stephan
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2022, 24 (01) : 67 - 87
[13] Extending a Brainiac Prover to Lambda-Free Higher-Order Logic
Vukmirovic, Petar
Blanchette, Jasmin Christian
Cruanes, Simon
Schulz, Stephan
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT I, 2019, 11427 : 192 - 210
[14] Extending a brainiac prover to lambda-free higher-order logic
Petar Vukmirović
Jasmin Blanchette
Simon Cruanes
Stephan Schulz
International Journal on Software Tools for Technology Transfer, 2022, 24 : 67 - 87
[15] Derivation lengths and order types of Knuth-Bendix orders
Lepper, I
THEORETICAL COMPUTER SCIENCE, 2001, 269 (1-2) : 433 - 450
[16] The decidability of the first-order theory of the Knuth-Bendix order in the case of unary signatures
Korovin, K
Voronkov, A
FST TCS 2002: FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEOETICAL COMPUTER SCIENCE, PROCEEDINGS, 2002, 2556 : 230 - 240
[17] Higher-order algebra with transfinite types
Steggles, LJ
HIGHER-ORDER ALGEBRA, LOGIC, AND TERM REWRITING, 1996, 1074 : 238 - 263
[18] THE SKYRME MODEL AND HIGHER-ORDER TERMS
MARLEAU, L
PHYSICS LETTERS B, 1990, 235 (1-2) : 141 - 146
[19] Higher-order terms in mode conversion
Swanson, DG
PHYSICS OF PLASMAS, 1998, 5 (07) : 2810 - 2812
[20] HIGHER-ORDER CURVATURE TERMS IN THEORIES WITH CREATION
WOLF, C
ASTRONOMISCHE NACHRICHTEN, 1988, 309 (03) : 173 - 175

← 1 2 3 4 5 →