Sledgehammer: Judgement Day

Sascha Böhme and Tobias Nipkow

Document: DOI PDF

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:

• Arrow
• NS
• Hoare
• Jinja
• SN
• FTA
• FFT

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}
}