The Sledgehammer: Let Automatic Theorem Provers write your Isabelle scripts!

sledgehammer   pic The sledgehammer can be used, at any point in a backward proof, with one mouse click. Your first subgoal will be converted into clause form and given to automatic theorem provers (ATPs), together with perhaps hundreds of other clauses representing currently known facts. Because jobs are run in the background, you can continue to work on your proof by other means. Provers can be run in parallel, the first successful result is displayed, and the other provers are terminated. Any reply (which may arrive minutes later) will appear in the Proof General response buffer. If a subgoal is proved, the response consists of a list of Isabelle commands to insert into the proof script. These will invoke the Metis prover.


Supported provers include E, SPASS, Vampire. Additionally, provers from System on TPTP can be queried over the internet. The standard Isabelle installation already includes bundled versions of E and SPASS. Remote Vampire is also preconfigured. Note that remote provers require Perl with the World Wide Web Library libwww-perl installed.

How to Invoke It

The sledgehammer is part of Isabelle/HOL. To call it, merely invoke the menu item Isabelle > Commands > sledgehammer (see screenshot). Alternatively, issue the sledgehammer Isar command.

For best results, first simplify your problem by calling auto or at least safe followed by simp_all. None of the ATPs contain arithmetic decision procedures. They are not especially good at heavy rewriting, but because they regard equations as undirected, they often prove theorems that require the reverse orientation of a rewrite rule. Higher-order problems can be tackled, but the success rate is better for first-order problems. You may get better results if you first simplify the problem to remove higher-order features.

Note that problems can be easy for auto and difficult for ATPs, but the reverse is also true, so don't be discouraged if your first attempts fail. Because the system refers to all theorems known to Isabelle, it is particularly suitable when your goal has a short proof from lemmas that you don't know about.

Additional Commands

Several Isar commands are available to control the sledgehammer.

Setting User Options

By default, the ATP is given all theorems in the system, automatically filtered for relevance. Information about types and type classes is also supplied.

User options are set in the menu Isabelle > Settings


Jia Meng, Claire Quigley and Kong Woei Susanto contributed to the project. Recent improvements are by Fabian Immler. Thanks to Joe Hurd for providing his Metis prover. Financial support was provided by the EPSRC, through the project Automation for Interactive Proof.