src/Doc/Sledgehammer/document/root.tex

 solvers.}
 %
 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
 \cite{sutcliffe-2000}. The supported SMT solvers are CVC3 \cite{cvc3}, CVC4
 \cite{cvc4}, veriT \cite{bouton-et-al-2009}, and Z3 \cite{z3}. These are always

 \label{installation}
 
 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.
 
 There are three main ways to install automatic provers on your machine:
 

 \texttt{/usr/local/spass-3.8ds}
 \postw
 
 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
 variable \texttt{CVC3\_\allowbreak SOLVER}, \texttt{CVC4\_\allowbreak SOLVER},
 \texttt{VERIT\_\allowbreak SOLVER}, or \texttt{Z3\_SOLVER} to the complete path

 higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
 with support for the TPTP typed higher-order syntax (THF0). To use LEO-II, set
 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
 environment variable \texttt{SATALLAX\_HOME} to the directory that contains the
 \texttt{satallax} executable. Sledgehammer requires version 2.2 or above.

 \item[\labelitemi] \textbf{\textit{remote\_iprover\_eq}:} The
 remote version of iProver-Eq runs on Geoff Sutcliffe's Miami servers
 \cite{sutcliffe-2000}.
 
 \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.