The Sledgehammer: Let Automatic Theorem Provers write your Isabelle scripts!
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. Remote versions of E, SPASS and Vampire are configured by default. The remote version of Vampire is particularly useful, since Vampire is not available for all platforms. Note that remote provers require Perl with the World Wide Web Library libwww-perl installed.
The following the following pre-compiled multi-platform version of E is for local installation. Local provers 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.
How to Invoke It
The sledgehammer is already 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.
sledgehammerprover1 ... proverN invokes the specified automated theorem provers in parallel on the first subgoal. The first successful prover will terminate the others.- The
print_atpscommand tells about admissible prover names. Provers with the prefixremotequery 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 remote_vampire". atp_infoprints information about presently running provers.atp_killterminates all running provers.ML_command {* set Toplevel.debug *}generates voluminous debugging information, which is better avoided.
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_atpscommand. 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.
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 ![{LP15} AT [cam.ac.uk]](LP15_cam_ac_uk.png)
, along with background information. The system can be configured to export proof files.
ML {* AtpWrapper.destdir := "/Users/lcp/mydir" *}sets a destination directory for export.ML {* AtpWrapper.problem_name := "george" *}specifies the prefix of the problems' filenames.
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.