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 条
  • [41] Height of a superposition
    Delhomme, Christian
    ORDER-A JOURNAL ON THE THEORY OF ORDERED SETS AND ITS APPLICATIONS, 2006, 23 (2-3): : 221 - 233
  • [42] Superposition Quantification
    Chang, Li-Na
    Luo, Shun-Long
    Sun, Yuan
    COMMUNICATIONS IN THEORETICAL PHYSICS, 2017, 68 (05) : 565 - 570
  • [43] SUPERPOSITION IN RHEOLOGY
    MARKOVITZ, H
    JOURNAL OF POLYMER SCIENCE PART C-POLYMER SYMPOSIUM, 1975, (50): : 431 - 456
  • [44] Topology in superposition
    K. Birgitta Whaley
    Nature Physics, 2012, 8 (1) : 9 - 10
  • [45] NONLINEAR SUPERPOSITION
    JONES, SE
    AMES, WF
    JOURNAL OF MATHEMATICAL ANALYSIS AND APPLICATIONS, 1967, 17 (03) : 484 - &
  • [46] Superposition Quantification
    常利娜
    骆顺龙
    孙源
    CommunicationsinTheoreticalPhysics, 2017, 68 (11) : 565 - 570
  • [47] Superposition by position
    Jin, Hui
    Laroia, Rajiv
    Richardson, Tom
    2006 IEEE INFORMATION THEORY WORKSHOP, 2006, : 222 - +
  • [48] Observing a superposition
    Skokowski, Paul
    SYNTHESE, 2021, 199 (3-4) : 7107 - 7129
  • [49] Functional superposition
    Sypniewski, BP
    TWENTY-THIRD LACUS FORUM 1996, 1997, : 279 - 287
  • [50] Height of a Superposition
    Christian Delhommé
    Order, 2006, 23 : 221 - 233
12345