Extending a brainiac prover to lambda-free higher-order logic

Petar Vukmirović; Jasmin Blanchette; Simon Cruanes; Stephan Schulz

doi:10.1007/s10009-021-00639-7

Extending a brainiac prover to lambda-free higher-order logic

Petar Vukmirović^*, Jasmin Blanchette, Simon Cruanes, Stephan Schulz

^*Corresponding author for this work

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

Abstract

Decades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem proving. Higher-order provers lag behind in terms of efficiency. Instead of developing a new higher-order prover from the ground up, we propose to start with the state-of-the-art superposition prover E and gradually enrich it with higher-order features. We explain how to extend the prover’s data structures, algorithms, and heuristics to λ-free higher-order logic, a formalism that supports partial application and applied variables. Our extension outperforms the traditional encoding and appears promising as a stepping stone toward full higher-order logic.

Original language	English
Pages (from-to)	67-87
Number of pages	21
Journal	International Journal on Software Tools for Technology Transfer
Volume	24
Issue number	1
Early online date	16 Aug 2021
DOIs	https://doi.org/10.1007/s10009-021-00639-7
Publication status	Published - Feb 2022

Bibliographical note

Funding Information:
Vukmirović and Blanchette’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). Blanchette has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (Project No. 016.Vidi.189.037, Lean Forward). He also benefited from the NWO Incidental Financial Support scheme.

Funding Information:
We are grateful to the maintainers of StarExec for letting us use their service. We thank Ahmed Bhayat, Alexander Bentkamp, Daniel El Ouraoui, Michael F?rber, Pascal Fontaine, Predrag Jani?i?, Robert Lewis, Tomer Libal, Giles Reger, Hans-J?rg Schurr, Alexander Steen, Mark Summerfield, Dmitriy Traytel, and the anonymous reviewers for suggesting many improvements to this text. We also want to thank the other members of the Matryoshka team, including Sophie Tourret and Uwe Waldmann, as well as Christoph Benzm?ller, Andrei Voronkov, Daniel Wand, and Christoph Weidenbach, for many stimulating discussions. Finally, we thank the TACAS 2019 chairs and editors of this special issue, Tom?? Vojnar and Lijun Zhang, for their patience with us.

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

Keywords

Automatic theorem provers
First-order logic
Higher-order logic

Access to Document

10.1007/s10009-021-00639-7

Handle.net

Persistent link

Cite this

@article{9b22fa5d62334f548b232aa44e2b4e59,

title = "Extending a brainiac prover to lambda-free higher-order logic",

abstract = "Decades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem proving. Higher-order provers lag behind in terms of efficiency. Instead of developing a new higher-order prover from the ground up, we propose to start with the state-of-the-art superposition prover E and gradually enrich it with higher-order features. We explain how to extend the prover{\textquoteright}s data structures, algorithms, and heuristics to λ-free higher-order logic, a formalism that supports partial application and applied variables. Our extension outperforms the traditional encoding and appears promising as a stepping stone toward full higher-order logic.",

keywords = "Automatic theorem provers, First-order logic, Higher-order logic",

author = "Petar Vukmirovi{\'c} and Jasmin Blanchette and Simon Cruanes and Stephan Schulz",

note = "Funding Information: Vukmirovi{\'c} and Blanchette{\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). Blanchette has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (Project No. 016.Vidi.189.037, Lean Forward). He also benefited from the NWO Incidental Financial Support scheme. Funding Information: We are grateful to the maintainers of StarExec for letting us use their service. We thank Ahmed Bhayat, Alexander Bentkamp, Daniel El Ouraoui, Michael F?rber, Pascal Fontaine, Predrag Jani?i?, Robert Lewis, Tomer Libal, Giles Reger, Hans-J?rg Schurr, Alexander Steen, Mark Summerfield, Dmitriy Traytel, and the anonymous reviewers for suggesting many improvements to this text. We also want to thank the other members of the Matryoshka team, including Sophie Tourret and Uwe Waldmann, as well as Christoph Benzm?ller, Andrei Voronkov, Daniel Wand, and Christoph Weidenbach, for many stimulating discussions. Finally, we thank the TACAS 2019 chairs and editors of this special issue, Tom?? Vojnar and Lijun Zhang, for their patience with us. Publisher Copyright: {\textcopyright} 2021, The Author(s).",

year = "2022",

month = feb,

doi = "10.1007/s10009-021-00639-7",

language = "English",

volume = "24",

pages = "67--87",

journal = "International Journal on Software Tools for Technology Transfer",

issn = "1433-2779",

publisher = "Springer Verlag",

number = "1",

}

TY - JOUR

T1 - Extending a brainiac prover to lambda-free higher-order logic

AU - Vukmirović, Petar

AU - Blanchette, Jasmin

AU - Cruanes, Simon

AU - Schulz, Stephan

N1 - Funding Information: Vukmirović and Blanchette’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). Blanchette has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (Project No. 016.Vidi.189.037, Lean Forward). He also benefited from the NWO Incidental Financial Support scheme. Funding Information: We are grateful to the maintainers of StarExec for letting us use their service. We thank Ahmed Bhayat, Alexander Bentkamp, Daniel El Ouraoui, Michael F?rber, Pascal Fontaine, Predrag Jani?i?, Robert Lewis, Tomer Libal, Giles Reger, Hans-J?rg Schurr, Alexander Steen, Mark Summerfield, Dmitriy Traytel, and the anonymous reviewers for suggesting many improvements to this text. We also want to thank the other members of the Matryoshka team, including Sophie Tourret and Uwe Waldmann, as well as Christoph Benzm?ller, Andrei Voronkov, Daniel Wand, and Christoph Weidenbach, for many stimulating discussions. Finally, we thank the TACAS 2019 chairs and editors of this special issue, Tom?? Vojnar and Lijun Zhang, for their patience with us. Publisher Copyright: © 2021, The Author(s).

PY - 2022/2

Y1 - 2022/2

N2 - Decades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem proving. Higher-order provers lag behind in terms of efficiency. Instead of developing a new higher-order prover from the ground up, we propose to start with the state-of-the-art superposition prover E and gradually enrich it with higher-order features. We explain how to extend the prover’s data structures, algorithms, and heuristics to λ-free higher-order logic, a formalism that supports partial application and applied variables. Our extension outperforms the traditional encoding and appears promising as a stepping stone toward full higher-order logic.

AB - Decades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem proving. Higher-order provers lag behind in terms of efficiency. Instead of developing a new higher-order prover from the ground up, we propose to start with the state-of-the-art superposition prover E and gradually enrich it with higher-order features. We explain how to extend the prover’s data structures, algorithms, and heuristics to λ-free higher-order logic, a formalism that supports partial application and applied variables. Our extension outperforms the traditional encoding and appears promising as a stepping stone toward full higher-order logic.

KW - Automatic theorem provers

KW - First-order logic

KW - Higher-order logic

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

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

U2 - 10.1007/s10009-021-00639-7

DO - 10.1007/s10009-021-00639-7

M3 - Article

AN - SCOPUS:85112573299

SN - 1433-2779

VL - 24

SP - 67

EP - 87

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

IS - 1

ER -

Extending a brainiac prover to lambda-free higher-order logic

Abstract

Bibliographical note

Keywords

Access to Document

Handle.net

Other files and links

Fingerprint

Cite this