--- a/doc-src/Sledgehammer/sledgehammer.tex Sun May 22 14:51:42 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Sun May 22 14:51:42 2011 +0200
@@ -79,13 +79,14 @@
Sledgehammer is a tool that applies first-order automatic theorem provers (ATPs)
and satisfiability-modulo-theories (SMT) solvers on the current goal. The
-supported ATPs are E \cite{schulz-2002}, SPASS \cite{weidenbach-et-al-2009},
-Vampire \cite{riazanov-voronkov-2002}, SInE-E \cite{sine}, SNARK \cite{snark},
-ToFoF-E \cite{tofof}, and Waldmeister \cite{waldmeister}. The ATPs are run
-either locally or remotely via the System\-On\-TPTP web service
+supported ATPs are E \cite{schulz-2002}, SInE-E \cite{sine}, SNARK \cite{snark},
+SPASS \cite{weidenbach-et-al-2009}, ToFoF-E \cite{tofof}, Vampire
+\cite{riazanov-voronkov-2002}, and Waldmeister \cite{waldmeister}. The ATPs are
+run either locally or remotely via the System\-On\-TPTP web service
\cite{sutcliffe-2000}. In addition to the ATPs, the SMT solvers Z3 \cite{z3} is
-used by default, and you can tell Sledgehammer to try Yices \cite{yices} and
-CVC3 \cite{cvc3} as well; these are run either locally or on a server in Munich.
+used by default, and you can tell Sledgehammer to try CVC3 \cite{cvc3} and Yices
+\cite{yices} as well; these are run either locally or on a server at the TU
+M\"unchen.
The problem passed to the automatic provers consists of your current goal
together with a heuristic selection of hundreds of facts (theorems) from the
@@ -199,9 +200,10 @@
\subsection{Installing SMT Solvers}
-CVC3, Yices, and Z3 can be run locally or remotely on a Munich server. If you
-want better performance and get the ability to replay proofs that rely on the
-\emph{smt} proof method, you should at least install Z3 locally.
+CVC3, Yices, and Z3 can be run locally or (for CVC3 and Z3) remotely on a TU
+M\"unchen server. If you want better performance and get the ability to replay
+proofs that rely on the \emph{smt} proof method, you should at least install Z3
+locally.
There are two main ways of installing SMT solvers locally.
@@ -230,7 +232,7 @@
\textbf{imports}~\textit{Main} \\
\textbf{begin} \\[2\smallskipamount]
%
-\textbf{lemma} ``$[a] = [b] \,\longleftrightarrow\, a = b$'' \\
+\textbf{lemma} ``$[a] = [b] \,\Longrightarrow\, a = b$'' \\
\textbf{sledgehammer}
\postw
@@ -242,39 +244,48 @@
\prew
\slshape
Sledgehammer: ``\textit{e}'' for subgoal 1: \\
-$([a] = [b]) = (a = b)$ \\
+$[a] = [b] \,\Longrightarrow\, a = b$ \\
+Try this command: \textbf{by} (\textit{metis last\_ConsL}). \\
+To minimize the number of lemmas, try this: \\
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{last\_ConsL}). \\[3\smallskipamount]
+%
+Sledgehammer: ``\textit{vampire}'' for subgoal 1: \\
+$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{vampire}] (\textit{hd.simps}). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{spass}'' for subgoal 1: \\
-$([a] = [b]) = (a = b)$ \\
-Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\
+$[a] = [b] \,\Longrightarrow\, a = b$ \\
+Try this command: \textbf{by} (\textit{metis list.inject}). \\
To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}]~(\textit{list.inject}). \\[3\smallskipamount]
%
-Sledgehammer: ``\textit{vampire}'' for subgoal 1: \\
-$([a] = [b]) = (a = b)$ \\
-Try this command: \textbf{by} (\textit{metis eq\_commute last\_snoc}). \\
+Sledgehammer: ``\textit{remote\_waldmeister}'' for subgoal 1: \\
+$[a] = [b] \,\Longrightarrow\, a = b$ \\
+Try this command: \textbf{by} (\textit{metis hd.simps insert\_Nil}). \\
To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{vampire}]~(\textit{eq\_commute last\_snoc}). \\[3\smallskipamount]
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_waldmeister}] \\
+\phantom{\textbf{sledgehammer}~}(\textit{hd.simps insert\_Nil}). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{remote\_sine\_e}'' for subgoal 1: \\
-$([a] = [b]) = (a = b)$ \\
+$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
To minimize the number of lemmas, try this: \\
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{remote\_z3}'' for subgoal 1: \\
-$([a] = [b]) = (a = b)$ \\
+$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}).
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_z3}]~(\textit{hd.simps}).
\postw
-Sledgehammer ran E, SPASS, Vampire, SInE-E, and Z3 in parallel. Depending on
-which provers are installed and how many processor cores are available, some of
-the provers might be missing or present with a \textit{remote\_} prefix.
+Sledgehammer ran E, SInE-E, SPASS, Vampire, Waldmeister, and Z3 in parallel.
+Depending on which provers are installed and how many processor cores are
+available, some of the provers might be missing or present with a
+\textit{remote\_} prefix. Waldmeister is run only for unit equational problems,
+where the goal's conclusion is a (universally quantified) equation.
For each successful prover, Sledgehammer gives a one-liner proof that uses the
\textit{metis} or \textit{smt} method. You can click the proof to insert it into
@@ -300,18 +311,19 @@
Sledgehammer and Metis. Frequently (and infrequently) asked questions are
answered in \S\ref{frequently-asked-questions}.
-\newcommand\point[1]{{\sl\bfseries#1}\par\nopagebreak}
+\newcommand\point[1]{\medskip\par{\sl\bfseries#1}\par\nopagebreak}
\point{Presimplify the goal}
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.
+least \textit{safe} followed by \textit{simp\_all}. The SMT solvers provide
+arithmetic decision procedures, but the ATPs typically do not (or if they do,
+Sledgehammer does not use it yet). Apart from Waldmeister, 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.
\point{Make sure at least E, SPASS, Vampire, and Z3 are installed}
@@ -363,6 +375,11 @@
\section{Frequently Asked Questions}
\label{frequently-asked-questions}
+This sections answers frequently (and infrequently) asked questions about
+Sledgehammer. It is a good idea to skim over it now even if you don't have any
+questions at this stage. And if you have any further questions not listed here,
+send them to the author at \authoremail.
+
\point{Why does Metis fail to reconstruct the proof?}
There are many reasons. If Metis runs seemingly forever, that is a sign that the
@@ -414,7 +431,7 @@
following:
\prew
-\textbf{lemma} ``$\forall x\> y\Colon{'}a.\ x = y \,\Longrightarrow \exists f\> g\Colon\mathit{nat} \Rightarrow {'}a.\ f \not= g$'' \\
+\textbf{lemma} ``$\forall x\> y\Colon{'}\!a.\ x = y \,\Longrightarrow \exists f\> g\Colon\mathit{nat} \Rightarrow {'}\!a.\ f \not= g$'' \\
\textbf{sledgehammer} [\textit{full\_types}] (\textit{nat.distinct\/}(1))
\postw
@@ -423,7 +440,7 @@
Briefly, the relevance filter assigns a score to every available fact (lemma,
theorem, definition, or axiom)\ based upon how many constants that fact shares
-with the conjecture; this process iterates to include facts relevant to those
+with the conjecture. This process iterates to include facts relevant to those
just accepted, but with a decay factor to ensure termination. The constants are
weighted to give unusual ones greater significance. The relevance filter copes
best when the conjecture contains some unusual constants; if all the constants
@@ -646,9 +663,15 @@
\begin{enum}
\opnodefault{provers}{string}
Specifies the automatic provers to use as a space-separated list (e.g.,
-``\textit{e}~\textit{spass}''). The following provers are supported:
+``\textit{e}~\textit{spass}''). The following local provers are supported:
\begin{enum}
+\item[$\bullet$] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
+Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
+set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
+executable, including the file name. Sledgehammer has been tested with version
+2.2.
+
\item[$\bullet$] \textbf{\textit{e}:} E is an ATP developed by Stephan Schulz
\cite{schulz-2002}. To use E, set the environment variable
\texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable,
@@ -662,44 +685,38 @@
download page. Sledgehammer requires version 3.5 or above. See
\S\ref{installation} for details.
+\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
+SRI \cite{yices}. To use Yices, set the environment variable
+\texttt{YICES\_SOLVER} to the complete path of the executable, including the
+file name. Sledgehammer has been tested with version 1.0.
+
\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use
Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory
that contains the \texttt{vampire} executable. Sledgehammer has been tested with
versions 11, 0.6, and 1.0.
-\item[$\bullet$] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
-Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
-set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
-executable, including the file name. Sledgehammer has been tested with version
-2.2.
-
-\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
-SRI \cite{yices}. To use Yices, set the environment variable
-\texttt{YICES\_SOLVER} to the complete path of the executable, including the
-file name. Sledgehammer has been tested with version 1.0.
-
\item[$\bullet$] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
Microsoft Research \cite{z3}. To use Z3, set the environment variable
\texttt{Z3\_SOLVER} to the complete path of the executable, including the file
-name. Sledgehammer has been tested with versions 2.7 to 2.18.
+name, and set \texttt{Z3\_NON\_COMMERCIAL=yes} to confirm that you are a
+noncommercial user. Sledgehammer has been tested with versions 2.7 to 2.18.
\item[$\bullet$] \textbf{\textit{z3\_atp}:} This version of Z3 pretends to be an
ATP, exploiting Z3's undocumented support for the TPTP format. It is included
for experimental purposes. It requires version 2.18 or above.
+\end{enum}
+
+In addition, the following remote provers are supported:
+
+\begin{enum}
+\item[$\bullet$] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
+on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
+point).
\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
-\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
-Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used.
-
-\item[$\bullet$] \textbf{\textit{remote\_tofof\_e}:} ToFoF-E is a metaprover
-developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
-servers. This ATP supports a fragment of the TPTP many-typed first-order format
-(TFF). It is supported primarily for experimenting with the
-\textit{type\_sys} $=$ \textit{simple} option (\S\ref{problem-encoding}).
-
\item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
SInE runs on Geoff Sutcliffe's Miami servers.
@@ -708,13 +725,19 @@
developed by Stickel et al.\ \cite{snark}. The remote version of
SNARK runs on Geoff Sutcliffe's Miami servers.
-\item[$\bullet$] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit
-equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. The remote
-version of Waldmeister runs on Geoff Sutcliffe's Miami servers.
+\item[$\bullet$] \textbf{\textit{remote\_tofof\_e}:} ToFoF-E is a metaprover
+developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
+servers. This ATP supports a fragment of the TPTP many-typed first-order format
+(TFF). It is supported primarily for experimenting with the
+\textit{type\_sys} $=$ \textit{simple} option (\S\ref{problem-encoding}).
-\item[$\bullet$] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
-on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
-point).
+\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
+Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used.
+
+\item[$\bullet$] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit
+equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be
+used to prove universally quantified equations using unconditional equations.
+The remote version of Waldmeister runs on Geoff Sutcliffe's Miami servers.
\item[$\bullet$] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to