Sledgehammer

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.

Installation

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.

sledgehammer prover₁ ... prover_N invokes the specified automated theorem provers in parallel on the first subgoal. The first successful prover will terminate the others.
The print_atps command tells about admissible prover names. Provers with the prefix remote query SystemOnTPTP, so an active internet connection is needed.
If no provers are given as arguments to sledgehammer, the system refers to the default which is set to "e spass remote_vampire".
atp_info prints information about presently running provers.
atp_kill terminates all running provers.

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

Isabelle > Settings > ATP: Provers sets the default provers. Valid prover names can be found by issuing the print_atps command. Several provers may be specified, for parallel execution. The default setting is "e remote_vampire".
Isabelle > Settings > ATP: Timeout sets the time limit for all prover processes. The default is 60.
Isabelle > Settings > ATP: Maximum Number sets the maximum number of independent prover processes. The default is 5. Excessive provers are automatically terminated.

Acknowledgments

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.