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 language | English |
---|---|
Title of host publication | Automated Deduction – CADE 2019 |
Subtitle of host publication | 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings |
Editors | Pascal Fontaine |
Publisher | Springer |
Pages | 55-73 |
Number of pages | 19 |
ISBN (Electronic) | 9783030294366 |
ISBN (Print) | 9783030294359 |
DOIs | |
Publication status | Published - 2019 |
Event | 27th International Conference on Automated Deduction, CADE 2019 - Natal, Brazil Duration: 27 Aug 2019 → 30 Aug 2019 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 11716 LNAI |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 27th International Conference on Automated Deduction, CADE 2019 |
---|---|
Country/Territory | Brazil |
City | Natal |
Period | 27/08/19 → 30/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).
Funders | Funder number |
---|---|
Horizon 2020 Framework Programme | 713999 |
European Research Council | |
Nederlandse Organisatie voor Wetenschappelijk Onderzoek | 016 |