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]

Andrews P.B, 1977, IJCAI, P566

[2]

[Anonymous], 2010, Archive of Formal Proofs

[3]

[Anonymous], 1998, Term Rewriting and All That

[4]

Aoto T, 2003, LECT NOTES COMPUT SC, V2706, P380

[5] Analytic Tableaux for Higher-Order Logic with Choice [J].

Backes, Julian ;

Brown, Chad Edward .

JOURNAL OF AUTOMATED REASONING, 2011, 47 (04) :451-479

[6] Generalised multisets for chemical programming [J].

Banatre, J. -P. ;

Fradet, P. ;

Radenac, Y. .

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2006, 16 (04) :557-580

[7]

Becker H, 2017, TRANSFINITE KNUTH BE

[8]

Beeson M, 2004, LECT NOTES ARTIF INT, V3097, P460

[9]

Benzmuller C., 1998, Automated Deduction - CADE-15. 15th International Conference on Automated Deduction. Proceedings, P56, DOI 10.1007/BFb0054248

[10]

Benzmuller C., 2014, Handbook of the History of Logic, Volume 9, Computational Logic, P215

← 1 2 3 4 5 →