--- a/src/Doc/Sledgehammer/document/root.tex Tue Nov 07 15:16:40 2017 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Tue Nov 07 15:16:41 2017 +0100
@@ -107,7 +107,7 @@
The supported ATPs are AgsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E
\cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF \cite{tofof}, iProver
\cite{korovin-2009}, iProver-Eq \cite{korovin-sticksel-2010}, LEO-II
-\cite{leo2}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS
+\cite{leo2}, Leo-III \cite{leo3}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS
\cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002},
Waldmeister \cite{waldmeister}, and Zipperposition \cite{cruanes-2014}.
The ATPs are run either locally or remotely via the System\-On\-TPTP web service
@@ -154,9 +154,9 @@
Sledgehammer is part of Isabelle, so you do not need to install it. However, it
relies on third-party automatic provers (ATPs and SMT solvers).
-Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Satallax, SPASS, Vampire, and
+Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, Vampire, and
Zipperposition can be run locally; in addition, AgsyHOL, E, E-SInE, E-ToFoF,
-iProver, iProver-Eq, LEO-II, Satallax, SNARK, Vampire, and Waldmeister are
+iProver, iProver-Eq, LEO-II, Leo-III, Satallax, SNARK, Vampire, and Waldmeister are
available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers
CVC3, CVC4, veriT, and Z3 can be run locally.
@@ -184,26 +184,26 @@
in it.
-\item[\labelitemi] If you prefer to build AgsyHOL, Alt-Ergo, E, LEO-II, or
+\item[\labelitemi] If you prefer to build AgsyHOL, Alt-Ergo, E, LEO-II, Leo-III, or
Satallax manually, or found a Vampire executable somewhere (e.g.,
\url{http://www.vprover.org/}), set the environment variable
\texttt{AGSYHOL\_HOME}, \texttt{E\_HOME}, \texttt{LEO2\_HOME},
-\texttt{SATALLAX\_HOME}, or
+\texttt{LEO3\_HOME}, \texttt{SATALLAX\_HOME}, or
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{agsyHOL},
\texttt{eprover} (and/or \texttt{eproof} or \texttt{eproof\_ram}),
-\texttt{leo}, \texttt{satallax}, or \texttt{vampire} executable;
+\texttt{leo}, \texttt{leo3}, \texttt{satallax}, or \texttt{vampire} executable;
for Alt-Ergo, set the
environment variable \texttt{WHY3\_HOME} to the directory that contains the
\texttt{why3} executable.
Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 2.0,
-LEO-II 1.3.4, Satallax 2.2 to 2.7, and Vampire 0.6 to 4.0.%
+LEO-II 1.3.4, Leo-III 1.1, Satallax 2.2 to 2.7, and Vampire 0.6 to 4.0.%
\footnote{Following the rewrite of Vampire, the counter for version numbers was
reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, 2.6, and 3.0 are more
recent than 9.0 or 11.5.}%
Since the ATPs' output formats are neither documented nor stable, other
versions might not work well with Sledgehammer. Ideally,
you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
-\texttt{SATALLAX\_VERSION}, or
+\texttt{LEO3\_VERSION}, \texttt{SATALLAX\_VERSION}, or
\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``4.0'').
Similarly, if you want to install CVC3, CVC4, veriT, or Z3, set the environment
@@ -787,6 +787,13 @@
the environment variable \texttt{LEO2\_HOME} to the directory that contains the
\texttt{leo} executable. Sledgehammer requires version 1.3.4 or above.
+\item[\labelitemi] \textbf{\textit{leo3}:} Leo-III is an automatic
+higher-order prover developed by Alexander Steen, Max Wisniewski, Christoph
+Benzm\"uller et al.\ \cite{leo3},
+with support for the TPTP typed higher-order syntax (THF0). To use Leo-III, set
+the environment variable \texttt{LEO3\_HOME} to the directory that contains the
+\texttt{leo3} executable. Sledgehammer requires version 1.1 or above.
+
\item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic
higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
support for the TPTP typed higher-order syntax (THF0). To use Satallax, set the
@@ -865,6 +872,9 @@
\item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
+\item[\labelitemi] \textbf{\textit{remote\_leo3}:} The remote version of Leo-III
+runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
+
\item[\labelitemi] \textbf{\textit{remote\_pirate}:} Pirate is a
highly experimental first-order resolution prover developed by Daniel Wand.
The remote version of Pirate run on a private server he generously set up.