Seventeen Provers under the Hammer
Résumé
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.
Fichier principal
paper.pdf (664.4 Ko)
Télécharger le fichier
image (1).png (948 B)
Télécharger le fichier
image.png (948 B)
Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)