Making Higher-Order Superposition Work

Petar Vukmirović; Alexander Bentkamp; Jasmin Blanchette; Simon Cruanes; Visa Nummelin; Sophie Tourret

doi:10.1007/s10817-021-09613-z

Making Higher-Order Superposition Work

Petar Vukmirović^*
, Alexander Bentkamp
, Jasmin Blanchette
, Simon Cruanes
, Visa Nummelin
, Sophie Tourret

^*Corresponding author for this work

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

139 Downloads (Pure)

Abstract

Superposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about Booleans, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.

Original language	English
Pages (from-to)	541-564
Number of pages	24
Journal	Journal of Automated Reasoning
Volume	66
Issue number	4
Early online date	17 Jan 2022
DOIs	https://doi.org/10.1007/s10817-021-09613-z
Publication status	Published - Nov 2022

Bibliographical note

Publisher Copyright:
© 2021, The Author(s), under exclusive licence to Springer Nature B.V.

Funding

We are grateful to the maintainers of StarExec for letting us use their service. Ahmed Bhayat and Giles Reger guided us through details of Vampire 4.5. Ahmed Bhayat, Michael F\u00E4rber, Mathias Fleury, Predrag Jani\u010Di\u0107, Mark Summerfield, and the anonymous reviewers suggested content, textual, and typesetting improvements. We thank them\u00A0all. Vukmirovi\u0107, Bentkamp, and Blanchette\u2019s research has received funding from the European Research Council (ERC) under the European Union\u2019s Horizon 2020 research and innovation program (Grant Agreement No. 713999, Matryoshka). Blanchette and Nummelin\u2019s research has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (Project No. 016.Vidi.189.037, Lean Forward). We are grateful to the maintainers of StarExec for letting us use their service. Ahmed Bhayat and Giles Reger guided us through details of Vampire 4.5. Ahmed Bhayat, Michael F\u00E4rber, Mathias Fleury, Predrag Jani\u010Di\u0107, Mark Summerfield, and the anonymous reviewers suggested content, textual, and typesetting improvements. We thank them all. Vukmirovi\u0107, Bentkamp, and Blanchette\u2019s research has received funding from the European Research Council (ERC) under the European Union\u2019s Horizon 2020 research and innovation program (Grant Agreement No. 713999, Matryoshka). Blanchette and Nummelin\u2019s research has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (Project No. 016.Vidi.189.037, Lean Forward).

Funders	Funder number
European Research Council
???publication-publication-funding-organisation-not-added???	016.Vidi.189.037, 016
Horizon 2020 Framework Programme	713999

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 7 Affordable and Clean Energy

Keywords

Heuristics
Higher-order theorem proving
Superposition
Zipperposition

Access to Document

10.1007/s10817-021-09613-z

Making Higher-Order Superposition WorkFinal published version, 774 KBLicence: Article 25fa Dutch Copyright Act

Persistent URL (handle)

Persistent link

Cite this

@article{49a734f9c9e94f8f8f647aafb5613cfc,

title = "Making Higher-Order Superposition Work",

abstract = "Superposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about Booleans, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.",

keywords = "Heuristics, Higher-order theorem proving, Superposition, Zipperposition",

author = "Petar Vukmirovi{\'c} and Alexander Bentkamp and Jasmin Blanchette and Simon Cruanes and Visa Nummelin and Sophie Tourret",

note = "Publisher Copyright: {\textcopyright} 2021, The Author(s), under exclusive licence to Springer Nature B.V.",

year = "2022",

month = nov,

doi = "10.1007/s10817-021-09613-z",

language = "English",

volume = "66",

pages = "541--564",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "4",

}

TY - JOUR

T1 - Making Higher-Order Superposition Work

AU - Vukmirović, Petar

AU - Bentkamp, Alexander

AU - Blanchette, Jasmin

AU - Cruanes, Simon

AU - Nummelin, Visa

AU - Tourret, Sophie

PY - 2022/11

Y1 - 2022/11

N2 - Superposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about Booleans, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.

AB - Superposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about Booleans, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.

KW - Heuristics

KW - Higher-order theorem proving

KW - Superposition

KW - Zipperposition

UR - https://www.scopus.com/pages/publications/85123108780

UR - https://www.scopus.com/pages/publications/85123108780#tab=citedBy

U2 - 10.1007/s10817-021-09613-z

DO - 10.1007/s10817-021-09613-z

M3 - Article

AN - SCOPUS:85123108780

SN - 0168-7433

VL - 66

SP - 541

EP - 564

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 4

ER -

Making Higher-Order Superposition Work

Abstract

Bibliographical note

Funding

UN SDGs

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this