2026-07-21T23:19:36Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16717 2024-03-06T10:58:08Z ddc:004 open_access

Seventeen Provers Under the Hammer Desharnais, Martin Vukmirović, Petar Blanchette, Jasmin Wenzel, Makarius Automatic theorem proving interactive theorem proving proof assistants 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Martin Desharnais and Petar Vukmirović and Jasmin Blanchette and Makarius Wenzel 2022 Is Part Of LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2022.8 urn:nbn:de:0030-drops-167178 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.8 eng https://creativecommons.org/licenses/by/4.0/legalcode