# HG changeset patch # User blanchet # Date 1306068702 -7200 # Node ID cb28abfde010bffa9fa0676acd8d0bb0c7d5708a # Parent 9e620869a576a4d24e47456702766459cea2934e slightly improved documentation diff -r 9e620869a576 -r cb28abfde010 doc-src/Sledgehammer/sledgehammer.tex --- 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