Superposition for Higher-Order Logic

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

doi:10.1007/s10817-022-09649-9

Superposition for Higher-Order Logic

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

^*Corresponding author for this work

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

47 Downloads (Pure)

Abstract

We recently designed two calculi as stepping stones towards superposition for full higher-order logic: Boolean-free λ-superposition and superposition for first-order logic with interpreted Booleans. Stepping on these stones, we finally reach a sound and refutationally complete calculus for higher-order logic with polymorphism, extensionality, Hilbert choice, and Henkin semantics. In addition to the complexity of combining the calculus’s two predecessors, new challenges arise from the interplay between λ-terms and Booleans. Our implementation in Zipperposition outperforms all other higher-order theorem provers and is on a par with an earlier, pragmatic prototype of Booleans in Zipperposition.

Original language	English
Article number	10
Pages (from-to)	1-54
Number of pages	54
Journal	Journal of Automated Reasoning
Volume	67
Issue number	1
Early online date	21 Jan 2023
DOIs	https://doi.org/10.1007/s10817-022-09649-9
Publication status	Published - Mar 2023

Bibliographical note

Funding Information:
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’s research has received funding from a Chinese Academy of Sciences President’s International Fellowship for Postdoctoral Researchers (grant No. 2021PT0015). Blanchette’s research has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).

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

Funding

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’s research has received funding from a Chinese Academy of Sciences President’s International Fellowship for Postdoctoral Researchers (grant No. 2021PT0015). Blanchette’s 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
Chinese Academy of Sciences	2021PT0015
Not added	016.Vidi.189.037, 016
Horizon 2020 Framework Programme	713999

Keywords

Higher-order logic
Refutational completeness
Superposition calculus

Access to Document

10.1007/s10817-022-09649-9

Bentkamp 2023_Superposition for Higher-Order LogicFinal published version, 891 KBLicence: Article 25fa Dutch Copyright Act

Persistent URL (handle)

Persistent link

Cite this

@article{a2af8466c8e04faeab07db8aecbdace7,

title = "Superposition for Higher-Order Logic",

abstract = "We recently designed two calculi as stepping stones towards superposition for full higher-order logic: Boolean-free λ-superposition and superposition for first-order logic with interpreted Booleans. Stepping on these stones, we finally reach a sound and refutationally complete calculus for higher-order logic with polymorphism, extensionality, Hilbert choice, and Henkin semantics. In addition to the complexity of combining the calculus{\textquoteright}s two predecessors, new challenges arise from the interplay between λ-terms and Booleans. Our implementation in Zipperposition outperforms all other higher-order theorem provers and is on a par with an earlier, pragmatic prototype of Booleans in Zipperposition.",

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

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

note = "Funding Information: 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{\textquoteright}s research has received funding from a Chinese Academy of Sciences President{\textquoteright}s International Fellowship for Postdoctoral Researchers (grant No. 2021PT0015). Blanchette{\textquoteright}s research has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). Publisher Copyright: {\textcopyright} 2023, The Author(s), under exclusive licence to Springer Nature B.V.",

year = "2023",

month = mar,

doi = "10.1007/s10817-022-09649-9",

language = "English",

volume = "67",

pages = "1--54",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "1",

}

TY - JOUR

T1 - Superposition for Higher-Order Logic

AU - Bentkamp, Alexander

AU - Blanchette, Jasmin

AU - Tourret, Sophie

AU - Vukmirović, Petar

N1 - Funding Information: 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’s research has received funding from a Chinese Academy of Sciences President’s International Fellowship for Postdoctoral Researchers (grant No. 2021PT0015). Blanchette’s research has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). Publisher Copyright: © 2023, The Author(s), under exclusive licence to Springer Nature B.V.

PY - 2023/3

Y1 - 2023/3

N2 - We recently designed two calculi as stepping stones towards superposition for full higher-order logic: Boolean-free λ-superposition and superposition for first-order logic with interpreted Booleans. Stepping on these stones, we finally reach a sound and refutationally complete calculus for higher-order logic with polymorphism, extensionality, Hilbert choice, and Henkin semantics. In addition to the complexity of combining the calculus’s two predecessors, new challenges arise from the interplay between λ-terms and Booleans. Our implementation in Zipperposition outperforms all other higher-order theorem provers and is on a par with an earlier, pragmatic prototype of Booleans in Zipperposition.

AB - We recently designed two calculi as stepping stones towards superposition for full higher-order logic: Boolean-free λ-superposition and superposition for first-order logic with interpreted Booleans. Stepping on these stones, we finally reach a sound and refutationally complete calculus for higher-order logic with polymorphism, extensionality, Hilbert choice, and Henkin semantics. In addition to the complexity of combining the calculus’s two predecessors, new challenges arise from the interplay between λ-terms and Booleans. Our implementation in Zipperposition outperforms all other higher-order theorem provers and is on a par with an earlier, pragmatic prototype of Booleans in Zipperposition.

KW - Higher-order logic

KW - Refutational completeness

KW - Superposition calculus

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

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

U2 - 10.1007/s10817-022-09649-9

DO - 10.1007/s10817-022-09649-9

M3 - Article

AN - SCOPUS:85146661607

SN - 0168-7433

VL - 67

SP - 1

EP - 54

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 1

M1 - 10

ER -

Superposition for Higher-Order Logic

Abstract

Bibliographical note

Funding

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this