1.1 --- a/doc-src/Nitpick/nitpick.tex Tue Jan 17 18:25:36 2012 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Tue Jan 17 18:25:36 2012 +0100
1.3 @@ -121,11 +121,6 @@
1.4 C-n. This is equivalent to entering the \textbf{nitpick} command with no
1.5 arguments in the theory text.
1.6
1.7 -Nitpick requires the Kodkodi package for Isabelle as well as a Java 1.6 virtual
1.8 -machine called \texttt{java}. To run Nitpick, you must also make sure that the
1.9 -theory \textit{Nitpick} is imported---this is rarely a problem in practice
1.10 -since it is part of \textit{Main}.
1.11 -
1.12 Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
1.13 Nitpick also provides an automatic mode that can be enabled via the ``Auto
1.14 Nitpick'' option from the ``Isabelle'' menu in Proof General. In this mode,
1.15 @@ -135,13 +130,16 @@
1.16 \newbox\boxA
1.17 \setbox\boxA=\hbox{\texttt{nospam}}
1.18
1.19 -The examples presented in this manual can be found
1.20 +\newcommand\authoremail{\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
1.21 +in.\allowbreak tum.\allowbreak de}}
1.22 +
1.23 +To run Nitpick, you must also make sure that the theory \textit{Nitpick} is
1.24 +imported---this is rarely a problem in practice since it is part of
1.25 +\textit{Main}. The examples presented in this manual can be found
1.26 in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_Examples/Manual\_Nits.thy} theory.
1.27 The known bugs and limitations at the time of writing are listed in
1.28 -\S\ref{known-bugs-and-limitations}. Comments and bug reports concerning Nitpick
1.29 -or this manual should be directed to
1.30 -\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
1.31 -in.\allowbreak tum.\allowbreak de}.
1.32 +\S\ref{known-bugs-and-limitations}. Comments and bug reports concerning either
1.33 +the tool or the manual should be directed to the author at \authoremail.
1.34
1.35 \vskip2.5\smallskipamount
1.36
1.37 @@ -149,21 +147,39 @@
1.38 suggesting several textual improvements.
1.39 % and Perry James for reporting a typo.
1.40
1.41 -%\section{Installation}
1.42 -%\label{installation}
1.43 -%
1.44 -%MISSING:
1.45 -%
1.46 -% * Nitpick is part of Isabelle/HOL
1.47 -% * but it relies on an external tool called Kodkodi (Kodkod wrapper)
1.48 -% * Two options:
1.49 -% * if you use a prebuilt Isabelle package, Kodkodi is automatically there
1.50 -% * if you work from sources, the latest Kodkodi can be obtained from ...
1.51 -% download it, install it in some directory of your choice (e.g.,
1.52 -% $ISABELLE_HOME/contrib/kodkodi), and add the absolute path to Kodkodi
1.53 -% in your .isabelle/etc/components file
1.54 -%
1.55 -% * If you're not sure, just try the example in the next section
1.56 +\section{Installation}
1.57 +\label{installation}
1.58 +
1.59 +Sledgehammer is part of Isabelle, so you don't need to install it. However, it
1.60 +relies on a third-party Kodkod front-end called Kodkodi as well as a Java
1.61 +virtual machine called \texttt{java} (version 1.5 or above).
1.62 +
1.63 +There are two main ways of installing Kodkodi:
1.64 +
1.65 +\begin{enum}
1.66 +\item[\labelitemi] If you installed an official Isabelle package,
1.67 +it should already include a properly setup version of Kodkodi.
1.68 +
1.69 +\item[\labelitemi] If you use a repository or snapshot version of Isabelle, you
1.70 +an official Isabelle package, you can download the Isabelle-aware Kodkodi package
1.71 +from \url{http://www21.in.tum.de/~blanchet/\#software}. Extract the archive, then add a
1.72 +line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}%
1.73 +\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
1.74 +startup. Its value can be retrieved by executing \texttt{isabelle}
1.75 +\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
1.76 +file with the absolute path to Kodkodi. For example, if the
1.77 +\texttt{components} file does not exist yet and you extracted Kodkodi to
1.78 +\texttt{/usr/local/kodkodi-1.5.1}, create it with the single line
1.79 +
1.80 +\prew
1.81 +\texttt{/usr/local/kodkodi-1.5.1}
1.82 +\postw
1.83 +
1.84 +(including an invisible newline character) in it.
1.85 +\end{enum}
1.86 +
1.87 +To check whether Kodkodi is successfully installed, you can try out the example
1.88 +in \S\ref{propositional-logic}.
1.89
1.90 \section{First Steps}
1.91 \label{first-steps}
1.92 @@ -212,9 +228,6 @@
1.93 \hbox{}\qquad\qquad $Q = \textit{False}$
1.94 \postw
1.95
1.96 -%FIXME: If you get the output:...
1.97 -%Then do such-and-such.
1.98 -
1.99 Nitpick can also be invoked on individual subgoals, as in the example below:
1.100
1.101 \prew
1.102 @@ -344,7 +357,8 @@
1.103 \prew
1.104 \textbf{sledgehammer} \\[2\smallskipamount]
1.105 {\slshape Sledgehammer: ``$e$'' on goal \\
1.106 -Try this: \textrm{by}~(\textit{metis~theI}) (42 ms).} \\[2\smallskipamount]
1.107 +Try this: \textbf{by}~(\textit{metis~theI}) (42 ms).} \\
1.108 +\hbox{}\qquad\vdots \\[2\smallskipamount]
1.109 \textbf{by}~(\textit{metis~theI\/})
1.110 \postw
1.111
1.112 @@ -2289,8 +2303,7 @@
1.113 Specifies whether genuine and quasi genuine counterexamples should be given to
1.114 Isabelle's \textit{auto} tactic to assess their validity. If a ``genuine''
1.115 counterexample is shown to be spurious, the user is kindly asked to send a bug
1.116 -report to the author at
1.117 -\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@in.tum.de}.
1.118 +report to the author at \authoremail.
1.119
1.120 \nopagebreak
1.121 {\small See also \textit{max\_genuine} (\S\ref{output-format}).}
2.1 --- a/doc-src/Sledgehammer/sledgehammer.tex Tue Jan 17 18:25:36 2012 +0100
2.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Jan 17 18:25:36 2012 +0100
2.3 @@ -12,6 +12,8 @@
2.4 %\usepackage[scaled=.85]{beramono}
2.5 \usepackage{../../lib/texinputs/isabelle,../iman,../pdfsetup}
2.6
2.7 +\newcommand\download{\url{http://www21.in.tum.de/~blanchet/\#software}}
2.8 +
2.9 \def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}}
2.10 \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$}
2.11
2.12 @@ -142,68 +144,93 @@
2.13 \label{installation}
2.14
2.15 Sledgehammer is part of Isabelle, so you don't need to install it. However, it
2.16 -relies on third-party automatic theorem provers (ATPs) and SMT solvers.
2.17 +relies on third-party automatic provers (ATPs and SMT solvers).
2.18
2.19 -\subsection{Installing ATPs}
2.20 -
2.21 -Currently, E, LEO-II, Satallax, SPASS, and Vampire can be run locally; in
2.22 +Among the ATPs, E, LEO-II, Satallax, SPASS, and Vampire can be run locally; in
2.23 addition, E, E-SInE, E-ToFoF, iProver, iProver-Eq, LEO-II, Satallax, SNARK,
2.24 Waldmeister, and Vampire are available remotely via System\-On\-TPTP
2.25 \cite{sutcliffe-2000}. If you want better performance, you should at least
2.26 install E and SPASS locally.
2.27
2.28 -There are three main ways to install ATPs on your machine:
2.29 +Among the SMT solvers, CVC3, Yices, and Z3 can be run locally, and CVC3 and Z3
2.30 +can be run remotely on a TU M\"unchen server. If you want better performance and
2.31 +get the ability to replay proofs that rely on the \emph{smt} proof method
2.32 +without an Internet connection, you should at least install Z3 locally.
2.33
2.34 +There are three main ways to install automatic provers on your machine:
2.35 +
2.36 +\begin{sloppy}
2.37 \begin{enum}
2.38 -\item[\labelitemi] If you installed an official Isabelle package with everything
2.39 -inside, it should already include properly setup executables for E and SPASS,
2.40 -ready to use.%
2.41 -\footnote{Vampire's license prevents us from doing the same for this otherwise
2.42 -wonderful tool.}
2.43 +\item[\labelitemi] If you installed an official Isabelle package, it should
2.44 +already include properly setup executables for CVC3, E, SPASS, and Z3, ready to use.%
2.45 +\footnote{Vampire's and Yices's licenses prevent us from doing the same for
2.46 +these otherwise remarkable tools.}
2.47 +For Z3, you must additionally set the variable
2.48 +\texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
2.49 +noncommercial user, either in the environment in which Isabelle is
2.50 +launched or in your
2.51 +\texttt{\char`\~/\$ISABELLE\_HOME\_USER/etc/settings} file.
2.52
2.53 -\item[\labelitemi] Alternatively, you can download the Isabelle-aware E and SPASS
2.54 -binary packages from Isabelle's download page. Extract the archives, then add a
2.55 -line to your \texttt{\$ISABELLE\_HOME\_USER/etc/components}%
2.56 +\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, E,
2.57 +SPASS, and Z3 binary packages from \download. Extract the archives, then add a
2.58 +line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}%
2.59 \footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
2.60 -startup. Its value can be retrieved by invoking \texttt{isabelle}
2.61 +startup. Its value can be retrieved by executing \texttt{isabelle}
2.62 \texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
2.63 -file with the absolute
2.64 -path to E or SPASS. For example, if the \texttt{components} does not exist yet
2.65 -and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create the
2.66 -\texttt{components} file with the single line
2.67 +file with the absolute path to CVC3, E, SPASS, or Z3. For example, if the
2.68 +\texttt{components} file does not exist yet and you extracted SPASS to
2.69 +\texttt{/usr/local/spass-3.7}, create it with the single line
2.70
2.71 \prew
2.72 \texttt{/usr/local/spass-3.7}
2.73 \postw
2.74
2.75 -in it.
2.76 +(including an invisible newline character) in it.
2.77
2.78 -\item[\labelitemi] If you prefer to build E or SPASS yourself, or found a
2.79 -Vampire executable somewhere (e.g., \url{http://www.vprover.org/}),
2.80 -set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
2.81 +\item[\labelitemi] If you prefer to build E, LEO-II, Satallax, or SPASS
2.82 +manually, or found a Vampire executable somewhere (e.g.,
2.83 +\url{http://www.vprover.org/}), set the environment variable \texttt{E\_HOME},
2.84 +\texttt{LEO2\_HOME}, \texttt{SATALLAX\_HOME}, \texttt{SPASS\_HOME}, or
2.85 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
2.86 -\texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
2.87 -with E 1.0 to 1.4, SPASS 3.5 and 3.7, and Vampire 0.6, 1.0, and 1.8%
2.88 +\texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable.
2.89 +Sledgehammer has been tested with E 1.0 to 1.4, LEO-II 1.2.9, Satallax 2.2,
2.90 +SPASS 3.5 and 3.7, and Vampire 0.6, 1.0, and 1.8%
2.91 \footnote{Following the rewrite of Vampire, the counter for version numbers was
2.92 reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent
2.93 -than, say, Vampire 9.0 or 11.5.}%
2.94 +than 9.0 or 11.5.}%
2.95 . Since the ATPs' output formats are neither documented nor stable, other
2.96 versions of the ATPs might not work well with Sledgehammer. Ideally,
2.97 -also set \texttt{E\_VERSION}, \texttt{SPASS\_VERSION}, or
2.98 -\texttt{VAMPIRE\_VERSION} to the ATP's version number (e.g., ``1.4'').
2.99 +also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
2.100 +\texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or
2.101 +\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``1.4'').
2.102 +
2.103 +Similarly, if you want to build CVC3, or found a
2.104 +Yices or Z3 executable somewhere (e.g.,
2.105 +\url{http://yices.csl.sri.com/download.shtml} or
2.106 +\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html}),
2.107 +set the environment variable \texttt{CVC3\_\allowbreak SOLVER},
2.108 +\texttt{YICES\_SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of
2.109 +the executable, \emph{including the file name}. Sledgehammer has been tested
2.110 +with CVC3 2.2, Yices 1.0.28, and Z3 3.0 to 3.2.
2.111 +Since the SMT solvers' output formats are somewhat unstable, other
2.112 +versions of the solvers might not work well with Sledgehammer. Ideally,
2.113 +also set \texttt{CVC3\_VERSION}, \texttt{YICES\_VERSION}, or
2.114 +\texttt{Z3\_VERSION} to the solver's version number (e.g., ``3.2'').
2.115 \end{enum}
2.116 +\end{sloppy}
2.117
2.118 -To check whether E and SPASS are successfully installed, follow the example in
2.119 -\S\ref{first-steps}. If the remote versions of E and SPASS are used (identified
2.120 -by the prefix ``\emph{remote\_}''), or if the local versions fail to solve the
2.121 -easy goal presented there, this is a sign that something is wrong with your
2.122 -installation.
2.123 +To check whether E, SPASS, Vampire, and/or Z3 are successfully installed, try
2.124 +out the example in \S\ref{first-steps}. If the remote versions of any of these
2.125 +provers is used (identified by the prefix ``\emph{remote\_\/}''), or if the
2.126 +local versions fail to solve the easy goal presented there, something must be
2.127 +wrong with the installation.
2.128
2.129 -Remote ATP invocation via the SystemOnTPTP web service requires Perl with the
2.130 -World Wide Web Library (\texttt{libwww-perl}) installed. If you must use a proxy
2.131 -server to access the Internet, set the \texttt{http\_proxy} environment variable
2.132 -to the proxy, either in the environment in which Isabelle is launched or in your
2.133 -\texttt{\char`\~/\$ISABELLE\_HOME\_USER/etc/settings} file. Here are a few examples:
2.134 +Remote prover invocation requires Perl with the World Wide Web Library
2.135 +(\texttt{libwww-perl}) installed. If you must use a proxy server to access the
2.136 +Internet, set the \texttt{http\_proxy} environment variable to the proxy, either
2.137 +in the environment in which Isabelle is launched or in your
2.138 +\texttt{\char`\~/\$ISABELLE\_HOME\_USER/etc/settings} file. Here are a few
2.139 +examples:
2.140
2.141 \prew
2.142 \texttt{http\_proxy=http://proxy.example.org} \\
2.143 @@ -211,45 +238,6 @@
2.144 \texttt{http\_proxy=http://joeblow:pAsSwRd@proxy.example.org}
2.145 \postw
2.146
2.147 -\subsection{Installing SMT Solvers}
2.148 -
2.149 -CVC3, Yices, and Z3 can be run locally or (for CVC3 and Z3) remotely on a TU
2.150 -M\"unchen server. If you want better performance and get the ability to replay
2.151 -proofs that rely on the \emph{smt} proof method, you should at least run Z3
2.152 -locally.
2.153 -
2.154 -There are two main ways of installing SMT solvers locally.
2.155 -
2.156 -\sloppy
2.157 -
2.158 -\begin{enum}
2.159 -\item[\labelitemi] If you installed an official Isabelle package with everything
2.160 -inside, it should already include properly setup executables for CVC3 and Z3,
2.161 -ready to use.%
2.162 -\footnote{Yices's license prevents us from doing the same for this otherwise
2.163 -wonderful tool.}
2.164 -For Z3, you must also set the variable
2.165 -\texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
2.166 -noncommercial user, either in the environment in which Isabelle is
2.167 -launched or in your
2.168 -\texttt{\char`\~/\$ISABELLE\_HOME\_USER/etc/settings} file.
2.169 -
2.170 -\item[\labelitemi] If you prefer to build CVC3 yourself, or found a
2.171 -Yices or Z3 executable somewhere (e.g.,
2.172 -\url{http://yices.csl.sri.com/download.shtml} or
2.173 -\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html}),
2.174 -set the environment variable \texttt{CVC3\_\allowbreak SOLVER},
2.175 -\texttt{YICES\_SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of
2.176 -the executable, including the file name. Sledgehammer has been tested
2.177 -with CVC3 2.2, Yices 1.0.28, and Z3 3.0 to 3.2.
2.178 -Since the SMT solvers' output formats are somewhat unstable, other
2.179 -versions of the solvers might not work well with Sledgehammer. Ideally,
2.180 -also set \texttt{CVC3\_VERSION}, \texttt{YICES\_VERSION}, or
2.181 -\texttt{Z3\_VERSION} to the solver's version number (e.g., ``3.2'').
2.182 -\end{enum}
2.183 -
2.184 -\fussy
2.185 -
2.186 \section{First Steps}
2.187 \label{first-steps}
2.188
2.189 @@ -272,29 +260,29 @@
2.190
2.191 \prew
2.192 \slshape
2.193 -Sledgehammer: ``\textit{e}'' on goal \\
2.194 +Sledgehammer: ``\textit{e\/}'' on goal \\
2.195 $[a] = [b] \,\Longrightarrow\, a = b$ \\
2.196 Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount]
2.197 %
2.198 -Sledgehammer: ``\textit{vampire}'' on goal \\
2.199 +Sledgehammer: ``\textit{z3\/}'' on goal \\
2.200 +$[a] = [b] \,\Longrightarrow\, a = b$ \\
2.201 +Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\[3\smallskipamount]
2.202 +%
2.203 +Sledgehammer: ``\textit{vampire\/}'' on goal \\
2.204 $[a] = [b] \,\Longrightarrow\, a = b$ \\
2.205 Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount]
2.206 %
2.207 -Sledgehammer: ``\textit{spass}'' on goal \\
2.208 +Sledgehammer: ``\textit{spass\/}'' on goal \\
2.209 $[a] = [b] \,\Longrightarrow\, a = b$ \\
2.210 Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount]
2.211 %
2.212 -Sledgehammer: ``\textit{remote\_waldmeister}'' on goal \\
2.213 +Sledgehammer: ``\textit{remote\_waldmeister\/}'' on goal \\
2.214 $[a] = [b] \,\Longrightarrow\, a = b$ \\
2.215 Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount]
2.216 %
2.217 -Sledgehammer: ``\textit{remote\_e\_sine}'' on goal \\
2.218 +Sledgehammer: ``\textit{remote\_e\_sine\/}'' on goal \\
2.219 $[a] = [b] \,\Longrightarrow\, a = b$ \\
2.220 -Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms). \\[3\smallskipamount]
2.221 -%
2.222 -Sledgehammer: ``\textit{remote\_z3}'' on goal \\
2.223 -$[a] = [b] \,\Longrightarrow\, a = b$ \\
2.224 -Try this: \textbf{by} (\textit{metis list.inject}) (20 ms).
2.225 +Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms).
2.226 \postw
2.227
2.228 Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, and Z3 in parallel.
2.229 @@ -326,7 +314,8 @@
2.230 Sledgehammer. Frequently (and infrequently) asked questions are answered in
2.231 \S\ref{frequently-asked-questions}.
2.232
2.233 -\newcommand\point[1]{\medskip\par{\sl\bfseries#1}\par\nopagebreak}
2.234 +%\newcommand\point[1]{\medskip\par{\sl\bfseries#1}\par\nopagebreak}
2.235 +\newcommand\point[1]{\subsection{\emph{#1}}}
2.236
2.237 \point{Presimplify the goal}
2.238
2.239 @@ -340,7 +329,7 @@
2.240 is better for first-order problems. Hence, you may get better results if you
2.241 first simplify the problem to remove higher-order features.
2.242
2.243 -\point{Make sure at least E, SPASS, Vampire, and Z3 are installed}
2.244 +\point{Make sure E, SPASS, Vampire, and Z3 are locally installed}
2.245
2.246 Locally installed provers are faster and more reliable than those running on
2.247 servers. See \S\ref{installation} for details on how to install them.
2.248 @@ -355,9 +344,9 @@
2.249 \item[\labelitemi] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies
2.250 the automatic provers (ATPs and SMT solvers) that should be run whenever
2.251 Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{e spass
2.252 -remote\_vampire}''). For convenience, you can omit ``\textit{provers}~=''
2.253 +remote\_vampire\/}''). For convenience, you can omit ``\textit{provers}~=''
2.254 and simply write the prover names as a space-separated list (e.g., ``\textit{e
2.255 -spass remote\_vampire}'').
2.256 +spass remote\_vampire\/}'').
2.257
2.258 \item[\labelitemi] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter})
2.259 specifies the maximum number of facts that should be passed to the provers. By
2.260 @@ -494,7 +483,7 @@
2.261 \textbf{sledgehammer}
2.262 \postw
2.263
2.264 -\point{Why are the generated Isar proofs so ugly/detailed/broken?}
2.265 +\point{Why are the generated Isar proofs so ugly/broken?}
2.266
2.267 The current implementation is experimental and explodes exponentially in the
2.268 worst case. Work on a new implementation has begun. There is a large body of
2.269 @@ -566,8 +555,8 @@
2.270
2.271 \prew
2.272 \slshape
2.273 -The prover found a type-unsound proof involving ``\textit{foo}'',
2.274 -``\textit{bar}'', and ``\textit{baz}'' even though a supposedly type-sound
2.275 +The prover found a type-unsound proof involving ``\textit{foo\/}'',
2.276 +``\textit{bar\/}'', and ``\textit{baz\/}'' even though a supposedly type-sound
2.277 encoding was used (or, less likely, your axioms are inconsistent). You might
2.278 want to report this to the Isabelle developers.
2.279 \postw
2.280 @@ -589,6 +578,8 @@
2.281 \section{Command Syntax}
2.282 \label{command-syntax}
2.283
2.284 +\subsection{Sledgehammer}
2.285 +
2.286 Sledgehammer can be invoked at any point when there is an open goal by entering
2.287 the \textbf{sledgehammer} command in the theory file. Its general syntax is as
2.288 follows:
2.289 @@ -636,7 +627,7 @@
2.290 Sledgehammer's behavior can be influenced by various \qty{options}, which can be
2.291 specified in brackets after the \textbf{sledgehammer} command. The
2.292 \qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
2.293 -\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true}'' is optional. For
2.294 +\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional. For
2.295 example:
2.296
2.297 \prew
2.298 @@ -671,6 +662,8 @@
2.299 (\S\ref{timeouts}) is superseded by the ``Auto Tools Time Limit'' in Proof
2.300 General's ``Isabelle'' menu. Sledgehammer's output is also more concise.
2.301
2.302 +\subsection{Metis}
2.303 +
2.304 The \textit{metis} proof method has the syntax
2.305
2.306 \prew
2.307 @@ -737,7 +730,7 @@
2.308
2.309 Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options
2.310 have a negated counterpart (e.g., \textit{blocking} vs.\
2.311 -\textit{non\_blocking}). When setting them, ``= \textit{true}'' may be omitted.
2.312 +\textit{non\_blocking}). When setting them, ``= \textit{true\/}'' may be omitted.
2.313
2.314 \subsection{Mode of Operation}
2.315 \label{mode-of-operation}
2.316 @@ -745,34 +738,37 @@
2.317 \begin{enum}
2.318 \opnodefaultbrk{provers}{string}
2.319 Specifies the automatic provers to use as a space-separated list (e.g.,
2.320 -``\textit{e}~\textit{spass}~\textit{remote\_vampire}''). The following local
2.321 +``\textit{e}~\textit{spass}~\textit{remote\_vampire\/}''). The following local
2.322 provers are supported:
2.323
2.324 \begin{enum}
2.325 \item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
2.326 Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
2.327 set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
2.328 -executable, including the file name. Sledgehammer has been tested with version
2.329 -2.2.
2.330 +executable, including the file name, or install the prebuilt CVC3 package from
2.331 +\download. Sledgehammer has been tested with version 2.2. See
2.332 +\S\ref{installation} for details.
2.333
2.334 \item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover
2.335 developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment
2.336 variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}
2.337 -executable, or install the prebuilt E package from Isabelle's download page. See
2.338 -\S\ref{installation} for details.
2.339 +executable, or install the prebuilt E package from \download. Sledgehammer has
2.340 +been tested with versions 1.0 to 1.4. See \S\ref{installation} for details.
2.341
2.342 \item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic
2.343 higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
2.344 -with support for the TPTP typed higher-order syntax (THF0). Sledgehammer
2.345 -requires version 1.2.9 or above.
2.346 +with support for the TPTP typed higher-order syntax (THF0). To use LEO-II, set
2.347 +the environment variable \texttt{LEO2\_HOME} to the directory that contains the
2.348 +\texttt{leo} executable. Sledgehammer requires version 1.2.9 or above.
2.349
2.350 \item[\labelitemi] \textbf{\textit{metis}:} Although it is much less powerful than
2.351 the external provers, Metis itself can be used for proof search.
2.352
2.353 \item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic
2.354 higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
2.355 -support for the TPTP typed higher-order syntax (THF0). Sledgehammer
2.356 -requires version 2.2 or above.
2.357 +support for the TPTP typed higher-order syntax (THF0). To use Satallax, set the
2.358 +environment variable \texttt{SATALLAX\_HOME} to the directory that contains the
2.359 +\texttt{satallax} executable. Sledgehammer requires version 2.2 or above.
2.360
2.361 \item[\labelitemi] \textbf{\textit{smt}:} The \textit{smt} proof method with the
2.362 current settings (usually:\ Z3 with proof reconstruction).
2.363 @@ -781,16 +777,16 @@
2.364 prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
2.365 To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
2.366 that contains the \texttt{SPASS} executable, or install the prebuilt SPASS
2.367 -package from Isabelle's download page. Sledgehammer requires version 3.5 or
2.368 -above. See \S\ref{installation} for details.
2.369 +package from \download. Sledgehammer requires version 3.5 or above. See
2.370 +\S\ref{installation} for details.
2.371
2.372 \item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution
2.373 prover developed by Andrei Voronkov and his colleagues
2.374 \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable
2.375 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
2.376 executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., ``1.8'').
2.377 -Sledgehammer has been tested with versions 0.6, 1.0, and 1.8. Vampire 1.8
2.378 -supports the TPTP typed first-order format (TFF0).
2.379 +Sledgehammer has been tested with versions 0.6, 1.0, and 1.8.
2.380 +%Vampire 1.8 supports the TPTP typed first-order format (TFF0).
2.381
2.382 \item[\labelitemi] \textbf{\textit{yices}:} Yices is an SMT solver developed at
2.383 SRI \cite{yices}. To use Yices, set the environment variable
2.384 @@ -1047,7 +1043,7 @@
2.385 and erases monotonic types, notably infinite types. (For \textit{mono\_simple},
2.386 the types are not actually erased but rather replaced by a shared uniform type
2.387 of individuals.) As argument to the \textit{metis} proof method, the question
2.388 -mark is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound}
2.389 +mark is replaced by a \hbox{``\textit{\_query\/}''} suffix. If the \emph{sound}
2.390 option is enabled, these encodings are fully sound.
2.391
2.392 \item[\labelitemi]
2.393 @@ -1057,14 +1053,14 @@
2.394 (quasi-sound):} \\
2.395 Even lighter versions of the `\hbox{?}' encodings. As argument to the
2.396 \textit{metis} proof method, the `\hbox{??}' suffix is replaced by
2.397 -\hbox{``\textit{\_query\_query}''}.
2.398 +\hbox{``\textit{\_query\_query\/}''}.
2.399
2.400 \item[\labelitemi]
2.401 \textbf{%
2.402 \textit{poly\_guards}@?, \textit{raw\_mono\_guards}@? (quasi-sound):} \\
2.403 Alternative versions of the `\hbox{??}' encodings. As argument to the
2.404 \textit{metis} proof method, the `\hbox{@?}' suffix is replaced by
2.405 -\hbox{``\textit{\_at\_query}''}.
2.406 +\hbox{``\textit{\_at\_query\/}''}.
2.407
2.408 \item[\labelitemi]
2.409 \textbf{%
2.410 @@ -1080,7 +1076,7 @@
2.411 and \textit{mono\_simple\_higher}, the types are not actually erased but rather
2.412 replaced by a shared uniform type of individuals.) As argument to the
2.413 \textit{metis} proof method, the exclamation mark is replaced by the suffix
2.414 -\hbox{``\textit{\_bang}''}.
2.415 +\hbox{``\textit{\_bang\/}''}.
2.416
2.417 \item[\labelitemi]
2.418 \textbf{%
2.419 @@ -1089,14 +1085,14 @@
2.420 (mildly unsound):} \\
2.421 Even lighter versions of the `\hbox{!}' encodings. As argument to the
2.422 \textit{metis} proof method, the `\hbox{!!}' suffix is replaced by
2.423 -\hbox{``\textit{\_bang\_bang}''}.
2.424 +\hbox{``\textit{\_bang\_bang\/}''}.
2.425
2.426 \item[\labelitemi]
2.427 \textbf{%
2.428 \textit{poly\_guards}@!, \textit{raw\_mono\_guards}@! (mildly unsound):} \\
2.429 Alternative versions of the `\hbox{!!}' encodings. As argument to the
2.430 \textit{metis} proof method, the `\hbox{@!}' suffix is replaced by
2.431 -\hbox{``\textit{\_at\_bang}''}.
2.432 +\hbox{``\textit{\_at\_bang\/}''}.
2.433
2.434 \item[\labelitemi] \textbf{\textit{smart}:} The actual encoding used depends on
2.435 the ATP and should be the most efficient virtually sound encoding for that ATP.
2.436 @@ -1113,7 +1109,7 @@
2.437 Specifies whether Sledgehammer should run in its fully sound mode. In that mode,
2.438 quasi-sound type encodings (which are the default) are made fully sound, at the
2.439 cost of some clutter in the generated problems. This option is ignored if
2.440 -\textit{type\_enc} is explicitly set to an unsound encoding.
2.441 +\textit{type\_enc} is set to an unsound encoding.
2.442 \end{enum}
2.443
2.444 \subsection{Relevance Filter}