Seventeen Provers Under the Hammer

Martin Desharnais; Petar Vukmirovic; Jasmin Blanchette; Makarius Wenzel

doi:10.5281/zenodo.5940084

Seventeen Provers Under the Hammer

Martin Desharnais^*, Petar Vukmirovic, Jasmin Blanchette, Makarius Wenzel

^*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

Abstract

One of the main success stories of automatic theorem provers has been their integration into proof assistants. Such integrations, or "hammers,"increase proof automation and hence user productivity. In this paper, we use Isabelle/HOL's Sledgehammer tool to find out how useful modern provers are at proving formulas in higher-order logic. Our evaluation follows in the steps of Böhme and Nipkow's Judgment Day study from 2010, but instead of three provers we use 17, including SMT solvers and higher-order provers. Our work offers an alternative yardstick for comparing modern provers, next to the benchmarks and competitions emerging from the TPTP World and SMT-LIB.

Original language	English
Title of host publication	13th International Conference on Interactive Theorem Proving (ITP 2022)
Editors	June Andronick, Leonardo de Moura
Place of Publication	Dagstuhl, Germany
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages	1-18
Number of pages	18
ISBN (Electronic)	9783959772525
DOIs	https://doi.org/10.5281/zenodo.5940084 https://doi.org/10.4230/LIPIcs.ITP.2022.8
Publication status	Published - 2022
Event	13th International Conference on Interactive Theorem Proving, ITP 2022 - Haifa, Israel Duration: 7 Aug 2022 → 10 Aug 2022

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Volume	237
ISSN (Print)	1868-8969

Conference

Conference	13th International Conference on Interactive Theorem Proving, ITP 2022
Country/Territory	Israel
City	Haifa
Period	7/08/22 → 10/08/22

Bibliographical note

Funding Information:
Funding This 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). Jasmin Blanchette: 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:
© Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel;.

Keywords

Automatic theorem proving
interactive theorem proving
proof assistants

UN SDGs

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

Access to Document

Persistent URL (handle)

Copy link address

Cite this

Desharnais, M., Vukmirovic, P., Blanchette, J., & Wenzel, M. (2022). Seventeen Provers Under the Hammer. In J. Andronick, & L. de Moura (Eds.), 13th International Conference on Interactive Theorem Proving (ITP 2022) (pp. 1-18). Article 8 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 237). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.5281/zenodo.5940084, https://doi.org/10.4230/LIPIcs.ITP.2022.8

Desharnais, Martin ; Vukmirovic, Petar ; Blanchette, Jasmin et al. / Seventeen Provers Under the Hammer. 13th International Conference on Interactive Theorem Proving (ITP 2022). editor / June Andronick ; Leonardo de Moura. Dagstuhl, Germany : Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2022. pp. 1-18 (Leibniz International Proceedings in Informatics, LIPIcs).

@inproceedings{74b70eb1d41e434094eb6cc49270c4f6,

title = "Seventeen Provers Under the Hammer",

abstract = "One of the main success stories of automatic theorem provers has been their integration into proof assistants. Such integrations, or {"}hammers,{"}increase proof automation and hence user productivity. In this paper, we use Isabelle/HOL's Sledgehammer tool to find out how useful modern provers are at proving formulas in higher-order logic. Our evaluation follows in the steps of B{\"o}hme and Nipkow's Judgment Day study from 2010, but instead of three provers we use 17, including SMT solvers and higher-order provers. Our work offers an alternative yardstick for comparing modern provers, next to the benchmarks and competitions emerging from the TPTP World and SMT-LIB. ",

keywords = "Automatic theorem proving, interactive theorem proving, proof assistants",

author = "Martin Desharnais and Petar Vukmirovic and Jasmin Blanchette and Makarius Wenzel",

note = "Funding Information: Funding This 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). Jasmin Blanchette: 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} Martin Desharnais, Petar Vukmirovi{\'c}, Jasmin Blanchette, and Makarius Wenzel;.; 13th International Conference on Interactive Theorem Proving, ITP 2022 ; Conference date: 07-08-2022 Through 10-08-2022",

year = "2022",

doi = "10.5281/zenodo.5940084",

language = "English",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

pages = "1--18",

editor = "June Andronick and {de Moura}, Leonardo",

booktitle = "13th International Conference on Interactive Theorem Proving (ITP 2022)",

}

Desharnais, M, Vukmirovic, P, Blanchette, J & Wenzel, M 2022, Seventeen Provers Under the Hammer. in J Andronick & L de Moura (eds), 13th International Conference on Interactive Theorem Proving (ITP 2022)., 8, Leibniz International Proceedings in Informatics, LIPIcs, vol. 237, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Dagstuhl, Germany, pp. 1-18, 13th International Conference on Interactive Theorem Proving, ITP 2022, Haifa, Israel, 7/08/22. https://doi.org/10.5281/zenodo.5940084, https://doi.org/10.4230/LIPIcs.ITP.2022.8

Seventeen Provers Under the Hammer. / Desharnais, Martin; Vukmirovic, Petar; Blanchette, Jasmin et al.
13th International Conference on Interactive Theorem Proving (ITP 2022). ed. / June Andronick; Leonardo de Moura. Dagstuhl, Germany: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2022. p. 1-18 8 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 237).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Seventeen Provers Under the Hammer

AU - Desharnais, Martin

AU - Vukmirovic, Petar

AU - Blanchette, Jasmin

AU - Wenzel, Makarius

N1 - Funding Information: Funding This 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). Jasmin Blanchette: 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: © Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel;.

PY - 2022

Y1 - 2022

N2 - One of the main success stories of automatic theorem provers has been their integration into proof assistants. Such integrations, or "hammers,"increase proof automation and hence user productivity. In this paper, we use Isabelle/HOL's Sledgehammer tool to find out how useful modern provers are at proving formulas in higher-order logic. Our evaluation follows in the steps of Böhme and Nipkow's Judgment Day study from 2010, but instead of three provers we use 17, including SMT solvers and higher-order provers. Our work offers an alternative yardstick for comparing modern provers, next to the benchmarks and competitions emerging from the TPTP World and SMT-LIB.

AB - One of the main success stories of automatic theorem provers has been their integration into proof assistants. Such integrations, or "hammers,"increase proof automation and hence user productivity. In this paper, we use Isabelle/HOL's Sledgehammer tool to find out how useful modern provers are at proving formulas in higher-order logic. Our evaluation follows in the steps of Böhme and Nipkow's Judgment Day study from 2010, but instead of three provers we use 17, including SMT solvers and higher-order provers. Our work offers an alternative yardstick for comparing modern provers, next to the benchmarks and competitions emerging from the TPTP World and SMT-LIB.

KW - Automatic theorem proving

KW - interactive theorem proving

KW - proof assistants

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

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

UR - https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=16717

U2 - 10.5281/zenodo.5940084

DO - 10.5281/zenodo.5940084

M3 - Conference contribution

AN - SCOPUS:85136094530

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 1

EP - 18

BT - 13th International Conference on Interactive Theorem Proving (ITP 2022)

A2 - Andronick, June

A2 - de Moura, Leonardo

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

CY - Dagstuhl, Germany

T2 - 13th International Conference on Interactive Theorem Proving, ITP 2022

Y2 - 7 August 2022 through 10 August 2022

ER -

Desharnais M, Vukmirovic P, Blanchette J, Wenzel M. Seventeen Provers Under the Hammer. In Andronick J, de Moura L, editors, 13th International Conference on Interactive Theorem Proving (ITP 2022). Dagstuhl, Germany: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2022. p. 1-18. 8. (Leibniz International Proceedings in Informatics, LIPIcs). Epub 2022 Aug 3. doi: 10.5281/zenodo.5940084, 10.4230/LIPIcs.ITP.2022.8

Seventeen Provers Under the Hammer

Abstract

Publication series

Conference

Bibliographical note

Keywords

UN SDGs

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this