--- 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}