# HG changeset patch # User blanchet # Date 1312875181 -7200 # Node ID d40e5c72b346e6b2b7d9f063ac60648aad25e0c4 # Parent 6ce82b9e2896bec8764fcb100d05909fc08f9e0b updated Sledgehammer docs diff -r 6ce82b9e2896 -r d40e5c72b346 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 09 09:24:34 2011 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 09 09:33:01 2011 +0200 @@ -85,15 +85,14 @@ Sledgehammer is a tool that applies automatic theorem provers (ATPs) and satisfiability-modulo-theories (SMT) solvers on the current goal. The -supported ATPs are E \cite{schulz-2002}, LEO-II \cite{leo2}, Satallax -\cite{satallax}, 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 CVC3 \cite{cvc3} and Yices -\cite{yices} as well; these are run either locally or on a server at the TU -M\"unchen. +supported ATPs are E \cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF +\cite{tofof}, LEO-II \cite{leo2}, Satallax \cite{satallax}, SNARK \cite{snark}, +SPASS \cite{weidenbach-et-al-2009}, 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 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 @@ -141,10 +140,10 @@ \subsection{Installing ATPs} -Currently, E, SPASS, and Vampire can be run locally; in addition, E, Vampire, -LEO-II, Satallax, SInE-E, SNARK, ToFoF-E, and Waldmeister are available remotely -via System\-On\-TPTP \cite{sutcliffe-2000}. If you want better performance, you -should at least install E and SPASS locally. +Currently, E, SPASS, and Vampire can be run locally; in addition, E, E-SInE, +E-ToFoF, LEO-II, Satallax, SNARK, Waldmeister, and Vampire are available +remotely via System\-On\-TPTP \cite{sutcliffe-2000}. If you want better +performance, you should at least install E and SPASS locally. There are three main ways to install ATPs on your machine: @@ -266,7 +265,7 @@ $[a] = [b] \,\Longrightarrow\, a = b$ \\ Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount] % -Sledgehammer: ``\textit{remote\_sine\_e}'' on goal \\ +Sledgehammer: ``\textit{remote\_e\_sine}'' on goal \\ $[a] = [b] \,\Longrightarrow\, a = b$ \\ Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms). \\[3\smallskipamount] % @@ -275,7 +274,7 @@ Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \postw -Sledgehammer ran E, SInE-E, SPASS, Vampire, Waldmeister, and Z3 in parallel. +Sledgehammer ran E, E-SInE, 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, @@ -771,6 +770,15 @@ \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\_e\_sine}:} E-SInE 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. + +\item[$\bullet$] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover +developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami +servers. This ATP supports the TPTP many-typed first-order format (TFF). The +remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers. + \item[$\bullet$] \textbf{\textit{remote\_leo2}:} LEO-II is an automatic higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2}, with support for the TPTP higher-order syntax (THF). The remote version of @@ -783,20 +791,11 @@ runs on Geoff Sutcliffe's Miami servers. In the current setup, the problems given to Satallax are only mildly higher-order. -\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. - \item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a first-order resolution prover developed by Stickel et al.\ \cite{snark}. It supports the TPTP many-typed first-order format (TFF). The remote version of SNARK 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 the TPTP many-typed first-order format (TFF). The -remote version of ToFoF-E runs on Geoff Sutcliffe's Miami servers. - \item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used. @@ -814,12 +813,12 @@ as an ATP'' runs on Geoff Sutcliffe's Miami servers. \end{enum} -By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever -the SMT module's \textit{smt\_solver} configuration option is set to) in -parallel---either locally or remotely, depending on the number of processor -cores available. For historical reasons, the default value of this option can be -overridden using the option ``Sledgehammer: Provers'' from the ``Isabelle'' menu -in Proof General. +By default, Sledgehammer will run E, E-SInE, SPASS, Vampire, Z3 (or whatever +the SMT module's \textit{smt\_solver} configuration option is set to), and (if +appropriate) Waldmeister in parallel---either locally or remotely, depending on +the number of processor cores available. For historical reasons, the default +value of this option can be overridden using the option ``Sledgehammer: +Provers'' from the ``Isabelle'' menu in Proof General. It is a good idea to run several provers in parallel, although it could slow down your machine. Running E, SPASS, and Vampire for 5~seconds yields a similar