summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Wed, 23 Jun 2010 15:06:40 +0200 | |

changeset 37517 | 19ba7ec5f1e3 |

parent 37516 | c81c86bfc18a |

child 37518 | efb0923cc098 |

steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs

--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Jun 23 14:36:23 2010 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Jun 23 15:06:40 2010 +0200 @@ -83,14 +83,19 @@ can be run locally or remotely via the SystemOnTPTP web service \cite{sutcliffe-2000}. -The problem passed to ATPs consists of the current goal together with a -heuristic selection of facts (theorems) from the current theory context, -filtered by relevance. The result of a successful ATP proof search is some -source text that usually (but not always) reconstructs the proof within -Isabelle, without requiring the ATPs again. The reconstructed proof relies on -the general-purpose Metis prover \cite{metis}, which is fully integrated into -Isabelle/HOL, with explicit inferences going through the kernel. Thus its -results are correct by construction. +The problem passed to ATPs consists of your current goal together with a +heuristic selection of hundreds of facts (theorems) from the current theory +context, filtered by relevance. Because jobs are run in the background, you can +continue to work on your proof by other means. Provers can be run in parallel. +Any reply (which may arrive minutes later) will appear in the Proof General +response buffer. + +The result of a successful ATP proof search is some source text that usually +(but not always) reconstructs the proof within Isabelle, without requiring the +ATPs again. The reconstructed proof relies on the general-purpose Metis prover +\cite{metis}, which is fully integrated into Isabelle/HOL, with explicit +inferences going through the kernel. Thus its results are correct by +construction. \newbox\boxA \setbox\boxA=\hbox{\texttt{nospam}} @@ -143,6 +148,9 @@ To check whether E and SPASS are installed, follow the example in \S\ref{first-steps}. +Remote ATP invocation via the SystemOnTPTP web service requires Perl with the +World Wide Web Library (\texttt{libwww-perl}) installed. + \section{First Steps} \label{first-steps} @@ -158,7 +166,10 @@ \textbf{sledgehammer} \postw -After a few seconds, Sledgehammer produces the following output: +Instead of issuing the \textbf{sledgehammer} command, you can also find +Sledgehammer in the ``Commands'' submenu of the ``Isabelle'' menu in Proof +General or press the Emacs key sequence C-c C-a C-s. +Either way, Sledgehammer produces the following output after a few seconds: \prew \slshape @@ -206,6 +217,23 @@ readable and also faster than the \textit{metis} one-liners. This feature is experimental. +\section{Hints} +\label{hints} + +For best results, first simplify your problem by calling \textit{auto} or at +least \textit{safe} followed by \textit{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 \textit{simp} rule. Higher-order problems +can be tackled, but the success rate is better for first-order problems. Hence, +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. + \section{Command Syntax} \label{command-syntax}