Superposition with Lambdas

被引：17
|
作者：
Bentkamp, Alexander [1 ]
Blanchette, Jasmin [1 ,2 ]
Tourret, Sophie [2 ]
Vukmirovic, Petar [1 ]
Waldmann, Uwe [2 ]
机构：
[1] Vrije Univ Amsterdam, Amsterdam, Netherlands
[2] Max Planck Inst Informat, Saarland Informat Campus, Saarbrucken, Germany
来源：
AUTOMATED DEDUCTION, CADE 27 | 2019年 / 11716卷
基金：
欧洲研究理事会;
关键词：
HIGHER-ORDER UNIFICATION; NORMAL-FORM;
D O I：
10.1007/978-3-030-29436-6_4
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We designed a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on beta eta-equivalence classes of.-terms and rely on higher-order unification to achieve refutational completeness. We implemented the calculus in the Zipperposition prover and evaluated it on TPTP and Isabelle benchmarks. The results suggest that superposition is a suitable basis for higher-order reasoning.
引用
收藏
页码：55 / 73
页数：19
相关论文
共 50 条
  • [21] POLARIZATION OF LAMBDAS AND BARLAMBDAS PRODUCED BY 400-GEV PROTONS
    HELLER, K
    COX, PT
    DWORKIN, J
    OVERSETH, OE
    SKUBIC, P
    SCHACHINGER, L
    DEVLIN, T
    EDELMAN, B
    EDWARDS, RT
    BUNCE, G
    HANDLER, R
    MARCH, R
    MARTIN, P
    PONDROM, L
    SHEAFF, M
    PHYSICAL REVIEW LETTERS, 1978, 41 (09) : 607 - 611
  • [22] LAMBDABEAM: Neural Program Search with Higher-Order Functions and Lambdas
    Shi, Kensen
    Dai, Hanjun
    Li, Wen-Ding
    Ellis, Kevin
    Sutton, Charles
    ADVANCES IN NEURAL INFORMATION PROCESSING SYSTEMS 36 (NEURIPS 2023), 2023,
  • [23] X-RAY WAVELENGTH CONVERSION FACTOR LAMBDA (LAMBDAG/LAMBDAS)
    BEARDEN, JA
    PHYSICAL REVIEW, 1965, 137 (1B): : B181 - &
  • [24] The Impact on Open Source Projects Due to C++ Templates and Lambdas:
    Shaikh, Bushra
    Jagtap, Vandana
    Pujeri, Uma
    Shukla, Ayush
    14th International Conference on Advances in Computing, Control, and Telecommunication Technologies, ACT 2023, 2023, 2023-June : 1530 - 1537
  • [25] Superposition
    Lucas-Pennington, Grace
    OVERLAND, 2020, (239): : 62 - 63
  • [26] SUPERPOSITION
    不详
    NATURE, 1973, 241 (5388) : 310 - 310
  • [27] Superposition
    Steeves, Nicole R.
    LIBRARY JOURNAL, 2015, 140 (05) : 87 - 87
  • [28] An Empirical Study on the Impact of C plus plus Lambdas and Programmer Experience
    Uesbeck, Phillip Merlin
    Stefik, Andreas
    Hanenberg, Stefan
    Pedersen, Jan
    Daleiden, Patrick
    2016 IEEE/ACM 38TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE), 2016, : 760 - 771
  • [29] Superposition
    Martinez-Medina, Andres
    I2 INVESTIGACION E INNOVACION EN ARQUITECTURA Y TERRITORIO, 2020, 8 (01):
  • [30] Is lambdas (λs) a good way of assessing the contribution of HLA to the overall genetics of IDDM?
    Tuomilehto-Wolf, E
    Tuomilehto, J
    DIABETOLOGIA, 1998, 41 : A78 - A78
12345