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 条
  • [1] Superposition with Lambdas
    Bentkamp, Alexander
    Blanchette, Jasmin
    Tourret, Sophie
    Vukmirovic, Petar
    Waldmann, Uwe
    JOURNAL OF AUTOMATED REASONING, 2021, 65 (07) : 893 - 940
  • [2] Superposition with Lambdas
    Alexander Bentkamp
    Jasmin Blanchette
    Sophie Tourret
    Petar Vukmirović
    Uwe Waldmann
    Journal of Automated Reasoning, 2021, 65 : 893 - 940
  • [3] The silence of the lambdas
    Garvey, James
    TPM-THE PHILOSOPHERS MAGAZINE, 2011, (55): : 19 - 27
  • [4] INTERACTIONS OF LAMBDAS WITH PROTONS
    ALEXANDER, G
    ANDERSON, JA
    CRAWFORD, FS
    LASKAR, W
    LLOYD, LJ
    PHYSICAL REVIEW LETTERS, 1961, 7 (09) : 348 - &
  • [5] Language, lambdas, and logic
    Muskens, R
    RESOURCE-SENSITIVITY BINDING AND ANAPHORA, 2003, 80 : 23 - 54
  • [6] Context Update for Lambdas and Vectors
    Muskens, Reinhard
    Sadrzadeh, Mehrnoosh
    LOGICAL ASPECTS OF COMPUTATIONAL LINGUISTICS: CELEBRATING 20 YEARS OF LACL (1996-2016), 2016, 10054 : 247 - 254
  • [7] Multi-layer Lambda Grid Properly Using Lambdas and Sub-lambdas
    Tsukishima, Yukio
    Sameshima, Yasunori
    Hirano, Akira
    Jinno, Masahiko
    Kudoh, Tomohiro
    Okazaki, Fumihiro
    2008 34TH EUROPEAN CONFERENCE ON OPTICAL COMMUNICATION (ECOC), 2008,
  • [8] Pipsqueak: Lean Lambdas with Large Libraries
    Oakes, Edward
    Yang, Leon
    Houck, Kevin
    Harter, Tyler
    Arpaci-Dusseau, Andrea C.
    Arpaci-Dusseau, Remzi H.
    2017 IEEE 37TH INTERNATIONAL CONFERENCE ON DISTRIBUTED COMPUTING SYSTEMS WORKSHOPS (ICDCSW), 2017, : 395 - 400
  • [9] Towards patterns for heaps and imperative lambdas
    Naumann, David A.
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2016, 85 (05) : 1038 - 1056
  • [10] The silence bleating! of the lambdas: Comment
    LaFrance, JT
    AMERICAN JOURNAL OF AGRICULTURAL ECONOMICS, 1998, 80 (01) : 221 - 230
12345