| Abstract: | Sledgehammer integrates third-party automatic theorem provers in the proof
assistant Isabelle/HOL. In the seven years since its first release in 2007, it
has grown to become an essential part of most Isabelle users' workflow. Although
a lot of work has gone into tuning the system, the main reason for
Sledgehammer's success is the impressive power of the external provers,
especially E, SPASS, Vampire, and Z3. In this paper, I review
Vampire's strengths and weaknesses in this context and propose a few
directions for future work. |
