Sledgehammer: Judgement Day

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.

• Type: Conference
• Year: 2010
• Where: CADE
• Authors: Sascha Böhme, Tobias Nipkow
• Keywords: CADE 2010, Diverse Isabelle Theories, Isabelle Proof Obligations, Logical Reasoning, Theorem Prover Isabelle