updated Sledgehammer docs
authorblanchet
Sat Sep 30 22:55:23 2017 +0200 (19 months ago)
changeset 667355887ae5b95a8
parent 66734 ea5bd1347d26
child 66736 148891036469
updated Sledgehammer docs
src/Doc/Sledgehammer/document/root.tex
     1.1 --- a/src/Doc/Sledgehammer/document/root.tex	Sat Sep 30 22:55:16 2017 +0200
     1.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Sat Sep 30 22:55:23 2017 +0200
     1.3 @@ -165,9 +165,7 @@
     1.4  \begin{sloppy}
     1.5  \begin{enum}
     1.6  \item[\labelitemi] If you installed an official Isabelle package, it should
     1.7 -already include properly setup executables for CVC4, E, SPASS, and Z3, ready to use.%
     1.8 -\footnote{Vampire's license prevents us from doing the same for
     1.9 -this otherwise remarkable tool.}
    1.10 +already include properly setup executables for CVC4, E, SPASS, veriT, and Z3, ready to use.
    1.11  
    1.12  \item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3,
    1.13  CVC4, E, SPASS, and Z3 binary packages from \download. Extract the archives,
    1.14 @@ -186,26 +184,26 @@
    1.15  
    1.16  in it.
    1.17  
    1.18 -\item[\labelitemi] If you prefer to build AgsyHOL, Alt-Ergo, E, LEO-II,
    1.19 -Satallax, or SPASS manually, or found a Vampire executable somewhere (e.g.,
    1.20 +\item[\labelitemi] If you prefer to build AgsyHOL, Alt-Ergo, E, LEO-II, or
    1.21 +Satallax manually, or found a Vampire executable somewhere (e.g.,
    1.22  \url{http://www.vprover.org/}), set the environment variable
    1.23  \texttt{AGSYHOL\_HOME}, \texttt{E\_HOME}, \texttt{LEO2\_HOME},
    1.24 -\texttt{SATALLAX\_HOME}, \texttt{SPASS\_HOME}, or
    1.25 +\texttt{SATALLAX\_HOME}, or
    1.26  \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{agsyHOL},
    1.27  \texttt{eprover} (and/or \texttt{eproof} or \texttt{eproof\_ram}),
    1.28 -\texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable;
    1.29 +\texttt{leo}, \texttt{satallax}, or \texttt{vampire} executable;
    1.30  for Alt-Ergo, set the
    1.31  environment variable \texttt{WHY3\_HOME} to the directory that contains the
    1.32  \texttt{why3} executable.
    1.33  Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 2.0,
    1.34 -LEO-II 1.3.4, Satallax 2.2 to 2.7, SPASS 3.8ds, and Vampire 0.6 to 4.0.%
    1.35 +LEO-II 1.3.4, Satallax 2.2 to 2.7, and Vampire 0.6 to 4.0.%
    1.36  \footnote{Following the rewrite of Vampire, the counter for version numbers was
    1.37  reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, 2.6, and 3.0 are more
    1.38  recent than 9.0 or 11.5.}%
    1.39  Since the ATPs' output formats are neither documented nor stable, other
    1.40  versions might not work well with Sledgehammer. Ideally,
    1.41  you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
    1.42 -\texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or
    1.43 +\texttt{SATALLAX\_VERSION}, or
    1.44  \texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``4.0'').
    1.45  
    1.46  Similarly, if you want to install CVC3, CVC4, veriT, or Z3, set the environment
    1.47 @@ -220,11 +218,11 @@
    1.48  \end{enum}
    1.49  \end{sloppy}
    1.50  
    1.51 -To check whether E, SPASS, Vampire, and/or Z3 are successfully installed, try
    1.52 -out the example in \S\ref{first-steps}. If the remote versions of any of these
    1.53 -provers is used (identified by the prefix ``\textit{remote\_\/}''), or if the
    1.54 -local versions fail to solve the easy goal presented there, something must be
    1.55 -wrong with the installation.
    1.56 +To check whether the provers are successfully installed, try out the example
    1.57 +in \S\ref{first-steps}. If the remote versions of any of these provers is used
    1.58 +(identified by the prefix ``\textit{remote\_\/}''), or if the local versions
    1.59 +fail to solve the easy goal presented there, something must be wrong with the
    1.60 +installation.
    1.61  
    1.62  Remote prover invocation requires Perl with the World Wide Web Library
    1.63  (\texttt{libwww-perl}) installed. If you must use a proxy server to access the
    1.64 @@ -312,11 +310,6 @@
    1.65  is better for first-order problems. Hence, you may get better results if you
    1.66  first simplify the problem to remove higher-order features.
    1.67  
    1.68 -\point{Make sure E, SPASS, Vampire, and Z3 are locally installed}
    1.69 -
    1.70 -Locally installed provers are faster and more reliable than those running on
    1.71 -servers. See \S\ref{installation} for details on how to install them.
    1.72 -
    1.73  \point{Familiarize yourself with the main options}
    1.74  
    1.75  Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of
    1.76 @@ -591,8 +584,8 @@
    1.77  theory to process all the available facts, learning from proofs generated by
    1.78  automatic provers. The prover to use and its timeout can be set using the
    1.79  \textit{prover} (\S\ref{mode-of-operation}) and \textit{timeout}
    1.80 -(\S\ref{timeouts}) options. It is recommended to perform learning using an
    1.81 -efficient first-order ATP (such as E, SPASS, and Vampire) as opposed to a
    1.82 +(\S\ref{timeouts}) options. It is recommended to perform learning using a
    1.83 +first-order ATP (such as E, SPASS, and Vampire) as opposed to a
    1.84  higher-order ATP or an SMT solver.
    1.85  
    1.86  \item[\labelitemi] \textbf{\textit{relearn\_isar}:} Same as \textit{unlearn}