Superposition with Lambdas

Alexander Bentkamp; Jasmin Blanchette; Sophie Tourret; Petar Vukmirović; Uwe Waldmann

doi:10.1007/s10817-021-09595-y

Superposition with Lambdas

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

^*Corresponding author for this work

Research output: Contribution to Journal › Article › Academic › peer-review

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
Pages (from-to)	893-940
Number of pages	48
Journal	Journal of Automated Reasoning
Volume	65
Issue number	7
Early online date	21 Aug 2021
DOIs	https://doi.org/10.1007/s10817-021-09595-y
Publication status	Published - Oct 2021

Bibliographical note

Funding Information:
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, Visa Nummelin, and Hans-Jörg Schurr were involved in many stimulating discussions. Christoph Weidenbach made this collaboration possible. Ahmed Bhayat, Wan Fokkink, Nicolas Peltier, Mark Summerfield, and the anonymous reviewers suggested several textual improvements. The maintainers of StarExec let us use their service for the evaluation. 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).

Publisher Copyright:
© 2021, The Author(s).

Copyright:
Copyright 2021 Elsevier B.V., All rights reserved.

Keywords

Higher-order logic
Refutational completeness
Superposition calculus

Access to Document

10.1007/s10817-021-09595-y

Persistent URL (handle)

Copy link address

Cite this

@article{0bb66062219b4f78b76f5f7d3e12d222,

title = "Superposition with Lambdas",

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.",

keywords = "Higher-order logic, Refutational completeness, Superposition calculus",

author = "Alexander Bentkamp and Jasmin Blanchette and Sophie Tourret and Petar Vukmirovi{\'c} and Uwe Waldmann",

note = "Funding Information: Simon Cruanes patiently explained Zipperposition{\textquoteright}s internals and allowed us to continue the development of his prover. Christoph Benzm{\"u}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, Visa Nummelin, and Hans-J{\"o}rg Schurr were involved in many stimulating discussions. Christoph Weidenbach made this collaboration possible. Ahmed Bhayat, Wan Fokkink, Nicolas Peltier, Mark Summerfield, and the anonymous reviewers suggested several textual improvements. The maintainers of StarExec let us use their service for the evaluation. We thank them all. Bentkamp, Blanchette, and Vukmirovi{\'c}{\textquoteright}s research has received funding from the European Research Council (ERC) under the European Union{\textquoteright}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). Publisher Copyright: {\textcopyright} 2021, The Author(s). Copyright: Copyright 2021 Elsevier B.V., All rights reserved.",

year = "2021",

month = oct,

doi = "10.1007/s10817-021-09595-y",

language = "English",

volume = "65",

pages = "893--940",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "7",

}

TY - JOUR

T1 - Superposition with Lambdas

AU - Bentkamp, Alexander

AU - Blanchette, Jasmin

AU - Tourret, Sophie

AU - Vukmirović, Petar

AU - Waldmann, Uwe

N1 - Funding Information: 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, Visa Nummelin, and Hans-Jörg Schurr were involved in many stimulating discussions. Christoph Weidenbach made this collaboration possible. Ahmed Bhayat, Wan Fokkink, Nicolas Peltier, Mark Summerfield, and the anonymous reviewers suggested several textual improvements. The maintainers of StarExec let us use their service for the evaluation. 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). Publisher Copyright: © 2021, The Author(s). Copyright: Copyright 2021 Elsevier B.V., All rights reserved.

PY - 2021/10

Y1 - 2021/10

N2 - 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.

AB - 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.

KW - Higher-order logic

KW - Refutational completeness

KW - Superposition calculus

UR - http://www.scopus.com/inward/record.url?scp=85103868001&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85103868001&partnerID=8YFLogxK

U2 - 10.1007/s10817-021-09595-y

DO - 10.1007/s10817-021-09595-y

M3 - Article

AN - SCOPUS:85103868001

SN - 0168-7433

VL - 65

SP - 893

EP - 940

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 7

ER -

Superposition with Lambdas

Abstract

Bibliographical note

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this