A Combinator-Based Superposition Calculus for Higher-Order Logic

被引：19

作者：

Bhayat, Ahmed ^{[1
]}

Reger, Giles ^{[1
]}

机构：

[1] Univ Manchester, Manchester, Lancs, England

来源：

AUTOMATED REASONING, PT I | 2020年 / 12166卷

关键词：

D O I：

10.1007/978-3-030-51074-9_16

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We present a refutationally complete superposition calculus for a version of higher-order logic based on the combinatory calculus. We also introduce a novel method of dealing with extensionality. The calculus was implemented in the Vampire theorem prover and we test its performance against other leading higher-order provers. The results suggest that the method is competitive.

引用

页码：278 / 296

页数：19

共 50 条

[41] Expressing First-Order π-Calculus in Higher-Order Calculus of Communicating Systems
徐贤
[J]. Journal of Computer Science & Technology, 2009, 24 (01) : 122 - 137
[42] Expressing First-Order π-Calculus in Higher-Order Calculus of Communicating Systems
Xian Xu
[J]. Journal of Computer Science and Technology, 2009, 24 : 122 - 137
[43] Expressing First-Order π-Calculus in Higher-Order Calculus of Communicating Systems
Xu, Xian
[J]. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2009, 24 (01) : 122 - 137
[44] On the Relationship between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic
Kobayashi, Naoki
Lozes, Etienne
Bruse, Florian
[J]. ACM SIGPLAN NOTICES, 2017, 52 (01) : 246 - 259
[45] CONTEXTUAL EQUIVALENCE FOR HIGHER-ORDER π-CALCULUS REVISITED
Jeffrey, Alan
Rathke, Julian
[J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2005, 1 (01)
[46] A core calculus of higher-order mixins and classes
Bettini, L
Bono, V
Likavec, S
[J]. TYPES FOR PROOFS AND PROGRAMS, 2004, 3085 : 83 - 98
[47] A Higher-Order Distributed Calculus with Name Creation
Pierard, Adrien
Sumii, Eijiro
[J]. 2012 27TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2012, : 531 - 540
[48] On Bisimulation Theory in Linear Higher-Order π-Calculus
Xu, Xian
[J]. TRANSACTIONS ON PETRI NETS AND OTHER MODELS OF CONCURRENCY III, 2009, 5800 : 244 - 274
[49] Higher-order matching in the linear λ-calculus with pairing
de Groote, P
Salvati, S
[J]. COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2004, 3210 : 220 - 234
[50] A higher-order duration calculus and its completeness
Zhan, NJ
[J]. SCIENCE IN CHINA SERIES E-TECHNOLOGICAL SCIENCES, 2000, 43 (06): : 625 - 640

← 1 2 3 4 5 →