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 条
  • [1] Superposition for Higher-Order Logic
    Bentkamp, Alexander
    Blanchette, Jasmin
    Tourret, Sophie
    Vukmirovic, Petar
    [J]. JOURNAL OF AUTOMATED REASONING, 2023, 67 (01)
  • [2] Superposition for Higher-Order Logic
    Alexander Bentkamp
    Jasmin Blanchette
    Sophie Tourret
    Petar Vukmirović
    [J]. Journal of Automated Reasoning, 2023, 67
  • [3] Superposition for Full Higher-order Logic
    Bentkamp, Alexander
    Blanchette, Jasmin
    Tourret, Sophie
    Vukmirovic, Petar
    [J]. AUTOMATED DEDUCTION, CADE 28, 2021, 12699 : 396 - 412
  • [4] Namespace logic: A logic for a reflective higher-order calculus
    Meredith, LG
    Radestock, M
    [J]. TRUSTWORTHY GLOBAL COMPUTING, 2005, 3705 : 353 - 369
  • [5] A Focused Sequent Calculus for Higher-Order Logic
    Lindblad, Fredrik
    [J]. AUTOMATED REASONING, IJCAR 2014, 2014, 8562 : 61 - 75
  • [6] Superposition for Lambda-Free Higher-Order Logic
    Bentkamp, Alexander
    Blanchette, Jasmin Christian
    Cruanes, Simon
    Waldmann, Uwe
    [J]. AUTOMATED REASONING, IJCAR 2018, 2018, 10900 : 28 - 46
  • [7] SUPERPOSITION FOR LAMBDA-FREE HIGHER-ORDER LOGIC
    Bentkamp, Alexander
    Blanchette, Jasmin
    Cruanes, Simon
    Waldmann, Uwe
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2021, 17 (02) : 1:1 - 1:38
  • [8] LOOPS IN COMBINATOR-BASED COMPILERS
    WAND, M
    [J]. INFORMATION AND CONTROL, 1983, 57 (2-3): : 148 - 164
  • [9] Towards the Formalization of Fractional Calculus in Higher-Order Logic
    Siddique, Umair
    Hasan, Osman
    Tahar, Sofiene
    [J]. INTELLIGENT COMPUTER MATHEMATICS, CICM 2015, 2015, 9150 : 316 - 324
  • [10] An untyped higher order logic with Y combinator
    Andrews, James H.
    [J]. JOURNAL OF SYMBOLIC LOGIC, 2007, 72 (04) : 1385 - 1404
12345