Superposition with lambdas

Alexander Bentkamp*, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, Uwe Waldmann

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

69 Downloads (Pure)

Abstract

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 βη-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.

Original languageEnglish
Title of host publicationAutomated Deduction – CADE 2019
Subtitle of host publication27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings
EditorsPascal Fontaine
PublisherSpringer
Pages55-73
Number of pages19
ISBN (Electronic)9783030294366
ISBN (Print)9783030294359
DOIs
Publication statusPublished - 2019
Event27th International Conference on Automated Deduction, CADE 2019 - Natal, Brazil
Duration: 27 Aug 201930 Aug 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11716 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference27th International Conference on Automated Deduction, CADE 2019
Country/TerritoryBrazil
CityNatal
Period27/08/1930/08/19

Funding

Simon Cruanes patiently explained Zipperposition?s internals and allowed us to continue the development of his prover. Christoph Benzm?ller and Alexander Steen shared insights and examples with us, guiding us through the literature and clarifying how the Leos work. Maria Paola Bonacina and Nicolas Peltier gave us some ideas on how to treat the extensionality axiom as a theory axiom, ideas we have yet to explore. Mathias Fleury helped us set up regression tests for Zipperposition. Ahmed Bhayat, Tomer Libal, and Enrico Tassi shared their insights on higher-order unification. Andrei Popescu and Dmitriy Traytel explained the terminology surrounding the ?-calculus. Haniel Barbosa, Daniel El Ouraoui, Pascal Fontaine, and Hans-J?rg Schurr were involved in many stimulating discussions. Christoph Weidenbach made this collaboration possible. Ahmed Bhayat, Mark Summerfield, and the anonymous reviewers suggested several textual improvements. We thank them all. Bentkamp, Blanchette, and Vukmirovi??s research has received funding from the European Research Council (ERC) under the European Union?s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Bentkamp and Blanchette also benefited from the Netherlands Organization for Scientific Research (NWO) Incidental Financial Support scheme. Blanchette has received funding from the NWO under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).

FundersFunder number
Horizon 2020 Framework Programme713999
European Research Council
Nederlandse Organisatie voor Wetenschappelijk Onderzoek016

    Fingerprint

    Dive into the research topics of 'Superposition with lambdas'. Together they form a unique fingerprint.

    Cite this