187 \footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at |
187 \footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at |
188 startup. Its value can be retrieved by executing \texttt{isabelle} |
188 startup. Its value can be retrieved by executing \texttt{isabelle} |
189 \texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.} |
189 \texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.} |
190 file with the absolute path to CVC3, E, SPASS, or Z3. For example, if the |
190 file with the absolute path to CVC3, E, SPASS, or Z3. For example, if the |
191 \texttt{components} file does not exist yet and you extracted SPASS to |
191 \texttt{components} file does not exist yet and you extracted SPASS to |
192 \texttt{/usr/local/spass-3.7}, create it with the single line |
192 \texttt{/usr/local/spass-3.8ds}, create it with the single line |
193 |
193 |
194 \prew |
194 \prew |
195 \texttt{/usr/local/spass-3.7} |
195 \texttt{/usr/local/spass-3.8ds} |
196 \postw |
196 \postw |
197 |
197 |
198 in it. |
198 in it. |
199 |
199 |
200 \item[\labelitemi] If you prefer to build E, LEO-II, Satallax, or SPASS |
200 \item[\labelitemi] If you prefer to build E, LEO-II, Satallax, or SPASS |
201 manually, or found a Vampire executable somewhere (e.g., |
201 manually, or found a Vampire executable somewhere (e.g., |
202 \url{http://www.vprover.org/}), set the environment variable \texttt{E\_HOME}, |
202 \url{http://www.vprover.org/}), set the environment variable \texttt{E\_HOME}, |
203 \texttt{LEO2\_HOME}, \texttt{SATALLAX\_HOME}, \texttt{SPASS\_HOME}, or |
203 \texttt{LEO2\_HOME}, \texttt{SATALLAX\_HOME}, \texttt{SPASS\_HOME}, or |
204 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof}, |
204 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof}, |
205 \texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable. |
205 \texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable. |
206 Sledgehammer has been tested with E 1.0 to 1.4, LEO-II 1.2.9, Satallax 2.2 and 2.3, |
206 Sledgehammer has been tested with E 1.0 to 1.4, LEO-II 1.2.9, Satallax 2.2 and~2.3, |
207 SPASS 3.5 and 3.7, and Vampire 0.6, 1.0, and 1.8% |
207 SPASS 3.5, 3.7, and 3.8ds, and Vampire 0.6, 1.0, and 1.8% |
208 \footnote{Following the rewrite of Vampire, the counter for version numbers was |
208 \footnote{Following the rewrite of Vampire, the counter for version numbers was |
209 reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent |
209 reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent |
210 than 9.0 or 11.5.}% |
210 than 9.0 or 11.5.}% |
211 . Since the ATPs' output formats are neither documented nor stable, other |
211 . Since the ATPs' output formats are neither documented nor stable, other |
212 versions of the ATPs might not work well with Sledgehammer. Ideally, |
212 versions might not work well with Sledgehammer. Ideally, |
213 also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION}, |
213 you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION}, |
214 \texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or |
214 \texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or |
215 \texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``1.4''). |
215 \texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``1.4''). |
216 |
216 |
217 Similarly, if you want to build Alt-Ergo or CVC3, or found a |
217 Similarly, if you want to build Alt-Ergo or CVC3, or found a |
218 Yices or Z3 executable somewhere (e.g., |
218 Yices or Z3 executable somewhere (e.g., |
823 |
823 |
824 \item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution |
824 \item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution |
825 prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}. |
825 prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}. |
826 To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory |
826 To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory |
827 that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the |
827 that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the |
828 version number (e.g., ``3.7''), or install the prebuilt SPASS package from |
828 version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from |
829 \download. Sledgehammer requires version 3.5 or above. |
829 \download. Sledgehammer requires version 3.5 or above. |
830 |
830 |
831 \item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution |
831 \item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution |
832 prover developed by Andrei Voronkov and his colleagues |
832 prover developed by Andrei Voronkov and his colleagues |
833 \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable |
833 \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable |