Sledgehammer: Judgement Day

Sascha Böhme Tobias Nipkow

Sledgehammer, a component of the interactive theorem prover Isabelle, finds proofs in higher-order logic by calling the automated provers for first-order logic E, SPASS and Vampire. This paper is the largest and most detailed empirical evaluation of such a link to date. Our test data consists of 1200 proof goals arising in 7 diverse Isabelle theories, thus representing typical Isabelle proof obligations. We measure the effectiveness of Sledgehammer and many other parameters such as run time and complexity of proofs. A facility for minimizing the number of facts needed to prove a goal is presented and analyzed.

pdf

BibTeX:

@inproceedings{Boehme-Nipkow-IJCAR10,author={Sascha B\"ohme and Tobias Nipkow},
title={Sledgehammer: Judgement Day},
booktitle={Automated Reasoning (IJCAR 2010)},
editor={J. Giesl and R. H\"ahnle},publisher={Springer},
series={LNCS},volume={6173},pages={107-121},year=2010}

Isabelle theories:

Data: