The Sledgehammer: Let Automatic Theorem Provers write your Isabelle scripts!
The sledgehammer can be used, at any point in a 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 run in the background, you can continue to work on your goals by other means. 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 and Vampire. E is the default; the following pre-compiled versions for common Linux and Mac OS X (Darwin) systems may be used:
| E prover executables | |
| E_x86-linux.tar.gz | 0.6 MB |
| E_x86-darwin.tar.gz | 0.6 MB |
| E_ppc-darwin.tar.gz | 0.5 MB |
The prover (or a symbolic link to it) should be installed in one of the following places:
| Isabelle setting | default value |
|---|---|
| E_HOME | $ISABELLE_HOME/contrib/E/$ML_PLATFORM/ |
| SPASS_HOME | $ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin/ |
| VAMPIRE_HOME | $ISABELLE_HOME/contrib/vampire/$ML_PLATFORM/ |
You can set these variables in your ~/isabelle/etc/settings file if you do not like the defaults. Use
- isatool getenv ML_PLATFORM
to inspect ML_PLATFORM (and analogously to inspect the other Isabelle settings).
How to Invoke It
The system is enabled by default. 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.
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. Numerous flags are available to modify this behavior, but they are chiefly useful for the developers.
Options are set as follows.
ML {* ResAtp.set_prover "vampire" *}sets the prover to Vampire. Also allowed is"spass". The default is"E".ML {* ResAtp.time_limit := 30 *}sets the time limit for each ATP process to 30 seconds. The default is 60.ML {* set Toplevel.debug *}generates voluminous debugging information.
How to Send Me Problems
If you have a problem that is not proved and you are certain that it should be, please send it to me (![{LP15} AT [cam.ac.uk]](LP15_cam_ac_uk.png)
), along with background information. The system can be configured to export proof files.
ML {* ResAtp.destdir := "/Users/lcp/mydir" *}sets a destination directory for export. IfResAtp.time_limitis set to zero, then ATPs are not called; the problem files are simply written to the given destination.ML {* ResAtp.problem_name := "george" *}specifies the prefix of the problems' filenames.
Acknowledgments
Jia Meng, Claire Quigley and Kong Woei Susanto contributed to the project. Thanks to Joe Hurd for providing his Metis prover. Financial support was provided by the EPSRC, through the project Automation for Interactive Proof.