Sledgehammer/document/root.tex

127 Isabelle > General.'' In this mode, a reduced version of Sledgehammer is run on
196 \texttt{LEO3\_VERSION}, or \texttt{SATALLAX\_VERSION} to the prover's version
207 \texttt{Z3\_VERSION} to the solver's version number (e.g., ``4.4.0'').
460 We hope to address this problem in a future version of Isabelle. In the
738 the \texttt{agsyHOL} executable. Sledgehammer has been tested with version 1.0.
756 prebuilt CVC4 package from \download. Sledgehammer has been tested with version
762 executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or
770 version 1.1.
780 \item[\labelitemi] \textbf{\textit{ehoh}:} Ehoh is an experimental version of
788 executables. Sledgehammer has been tested with version 0.99.
795 executables. Sledgehammer has been tested with version 0.8.
801 \texttt{leo} executable. Sledgehammer requires version 1.3.4 or above.
808 \texttt{leo3} executable. Sledgehammer requires version 1.1 or above.
814 \texttt{satallax} executable. Sledgehammer requires version 2.2 or above.
820 version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from
821 \download. Sledgehammer requires version 3.8ds or above.
827 executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g.,
836 file name. Sledgehammer has been tested with version smtcomp2014.
841 file name. Sledgehammer has been tested with a pre-release version of 4.4.0.
843 \item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
846 version 4.3.1 of Z3 or above. To use it, set the environment variable
862 \item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of
865 \item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs
875 remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.
878 remote version of iProver runs on Geoff Sutcliffe's Miami servers
882 remote version of iProver-Eq runs on Geoff Sutcliffe's Miami servers
885 \item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
888 \item[\labelitemi] \textbf{\textit{remote\_leo3}:} The remote version of Leo-III
893 The remote version of Pirate run on a private server he generously set up.
895 \item[\labelitemi] \textbf{\textit{remote\_satallax}:} The remote version of
900 TPTP typed first-order format (TFF0). The remote version of SNARK runs on
903 \item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of
909 corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister