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] 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
  • [43] CONTEXTUAL EQUIVALENCE FOR HIGHER-ORDER π-CALCULUS REVISITED
    Jeffrey, Alan
    Rathke, Julian
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2005, 1 (01)
  • [44] 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
  • [45] 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
  • [46] A higher-order duration calculus and its completeness
    Zhan, NJ
    [J]. SCIENCE IN CHINA SERIES E-TECHNOLOGICAL SCIENCES, 2000, 43 (06): : 625 - 640
  • [47] 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
  • [48] Higher-order matching in the linear λ-calculus with pairing
    de Groote, P
    Salvati, S
    [J]. COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2004, 3210 : 220 - 234
  • [49] Encodability and Separation for a Reflective Higher-Order Calculus
    Lybech, Stian
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2022, (368): : 95 - 112
  • [50] A Higher-Order Graph Calculus for Autonomic Computing
    Andrei, Oana
    Kirchner, Helene
    [J]. GRAPH THEORY, COMPUTATIONAL INTELLIGENCE AND THOUGHT: ESSAYS DEDICATED TO MARTIN CHARLES GOLUMBIC ON THE OCCASION OF HIS 60TH BIRTHDAY, 2009, 5420 : 15 - +
12345