src/Doc/Sledgehammer/document/root.tex
changeset 67021 41f1f8c4259b
parent 66735 5887ae5b95a8
child 68250 c45067867860
     1.1 --- a/src/Doc/Sledgehammer/document/root.tex	Tue Nov 07 15:16:40 2017 +0100
     1.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Tue Nov 07 15:16:41 2017 +0100
     1.3 @@ -107,7 +107,7 @@
     1.4  The supported ATPs are AgsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E
     1.5  \cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF \cite{tofof}, iProver
     1.6  \cite{korovin-2009}, iProver-Eq \cite{korovin-sticksel-2010}, LEO-II
     1.7 -\cite{leo2}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS
     1.8 +\cite{leo2}, Leo-III \cite{leo3}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS
     1.9  \cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002},
    1.10  Waldmeister \cite{waldmeister}, and Zipperposition \cite{cruanes-2014}.
    1.11  The ATPs are run either locally or remotely via the System\-On\-TPTP web service
    1.12 @@ -154,9 +154,9 @@
    1.13  Sledgehammer is part of Isabelle, so you do not need to install it. However, it
    1.14  relies on third-party automatic provers (ATPs and SMT solvers).
    1.15  
    1.16 -Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Satallax, SPASS, Vampire, and
    1.17 +Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, Vampire, and
    1.18  Zipperposition can be run locally; in addition, AgsyHOL, E, E-SInE, E-ToFoF,
    1.19 -iProver, iProver-Eq, LEO-II, Satallax, SNARK, Vampire, and Waldmeister are
    1.20 +iProver, iProver-Eq, LEO-II, Leo-III, Satallax, SNARK, Vampire, and Waldmeister are
    1.21  available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers
    1.22  CVC3, CVC4, veriT, and Z3 can be run locally.
    1.23  
    1.24 @@ -184,26 +184,26 @@
    1.25  
    1.26  in it.
    1.27  
    1.28 -\item[\labelitemi] If you prefer to build AgsyHOL, Alt-Ergo, E, LEO-II, or
    1.29 +\item[\labelitemi] If you prefer to build AgsyHOL, Alt-Ergo, E, LEO-II, Leo-III, or
    1.30  Satallax manually, or found a Vampire executable somewhere (e.g.,
    1.31  \url{http://www.vprover.org/}), set the environment variable
    1.32  \texttt{AGSYHOL\_HOME}, \texttt{E\_HOME}, \texttt{LEO2\_HOME},
    1.33 -\texttt{SATALLAX\_HOME}, or
    1.34 +\texttt{LEO3\_HOME}, \texttt{SATALLAX\_HOME}, or
    1.35  \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{agsyHOL},
    1.36  \texttt{eprover} (and/or \texttt{eproof} or \texttt{eproof\_ram}),
    1.37 -\texttt{leo}, \texttt{satallax}, or \texttt{vampire} executable;
    1.38 +\texttt{leo}, \texttt{leo3}, \texttt{satallax}, or \texttt{vampire} executable;
    1.39  for Alt-Ergo, set the
    1.40  environment variable \texttt{WHY3\_HOME} to the directory that contains the
    1.41  \texttt{why3} executable.
    1.42  Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 2.0,
    1.43 -LEO-II 1.3.4, Satallax 2.2 to 2.7, and Vampire 0.6 to 4.0.%
    1.44 +LEO-II 1.3.4, Leo-III 1.1, Satallax 2.2 to 2.7, and Vampire 0.6 to 4.0.%
    1.45  \footnote{Following the rewrite of Vampire, the counter for version numbers was
    1.46  reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, 2.6, and 3.0 are more
    1.47  recent than 9.0 or 11.5.}%
    1.48  Since the ATPs' output formats are neither documented nor stable, other
    1.49  versions might not work well with Sledgehammer. Ideally,
    1.50  you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
    1.51 -\texttt{SATALLAX\_VERSION}, or
    1.52 +\texttt{LEO3\_VERSION}, \texttt{SATALLAX\_VERSION}, or
    1.53  \texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``4.0'').
    1.54  
    1.55  Similarly, if you want to install CVC3, CVC4, veriT, or Z3, set the environment
    1.56 @@ -787,6 +787,13 @@
    1.57  the environment variable \texttt{LEO2\_HOME} to the directory that contains the
    1.58  \texttt{leo} executable. Sledgehammer requires version 1.3.4 or above.
    1.59  
    1.60 +\item[\labelitemi] \textbf{\textit{leo3}:} Leo-III is an automatic
    1.61 +higher-order prover developed by Alexander Steen, Max Wisniewski, Christoph
    1.62 +Benzm\"uller et al.\ \cite{leo3},
    1.63 +with support for the TPTP typed higher-order syntax (THF0). To use Leo-III, set
    1.64 +the environment variable \texttt{LEO3\_HOME} to the directory that contains the
    1.65 +\texttt{leo3} executable. Sledgehammer requires version 1.1 or above.
    1.66 +
    1.67  \item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic
    1.68  higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
    1.69  support for the TPTP typed higher-order syntax (THF0). To use Satallax, set the
    1.70 @@ -865,6 +872,9 @@
    1.71  \item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
    1.72  runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
    1.73  
    1.74 +\item[\labelitemi] \textbf{\textit{remote\_leo3}:} The remote version of Leo-III
    1.75 +runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
    1.76 +
    1.77  \item[\labelitemi] \textbf{\textit{remote\_pirate}:} Pirate is a
    1.78  highly experimental first-order resolution prover developed by Daniel Wand.
    1.79  The remote version of Pirate run on a private server he generously set up.