Sledgehammer: Judgement Day
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: