Abstract
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 1240 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. © 2010 Springer-Verlag.
Cite
CITATION STYLE
Böhme, S., & Nipkow, T. (2010). Sledgehammer: Judgement day. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6173 LNAI, pp. 107–121). https://doi.org/10.1007/978-3-642-14203-1_9
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
