Sledgehammer: Judgement Day
Sascha Böhme and Tobias Nipkow
Abstract: Sledgehammer, a component of the interactive theorem prover Isabelle, allows to prove goals 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 but also 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.
Isabelle theories:
Data:
- TPTP problems: TPTP.tar.gz (16 MB)
- Log files: Logs.tar.gz (1.2 MB)
Bibtex entry:
@inproceedings{ author = {B{\"o}hme, Sascha and Nipkow, Tobias}, title = {Sledgehammer: Judgement Day}, booktitle = {Automated Reasoning}, editor = {Giesl, J{\"u}rgen and H{\"a}hnle, Reiner}, series = {Lecture Notes in Computer Science}, volume = {6173}, year = 2010, pages = {107-121}, publisher = {Springer}, doi = {http://dx.doi.org/10.1007/978-3-642-14203-1_9} }