--- a/doc-src/Sledgehammer/sledgehammer.tex Mon Aug 06 22:12:17 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Mon Aug 06 22:12:17 2012 +0200
@@ -839,6 +839,7 @@
The following local provers are supported:
+\begin{sloppy}
\begin{enum}
\item[\labelitemi] \textbf{\textit{alt\_ergo}:} Alt-Ergo is a polymorphic
SMT solver developed by Bobot et al.\ \cite{alt-ergo}.
@@ -867,6 +868,19 @@
that contains the \texttt{emales.py} script. Sledgehammer has been tested with
version 1.1.
+\item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure
+instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}.
+To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the
+directory that contains the \texttt{iprover} executable. Sledgehammer has been
+tested with version 0.99.
+
+\item[\labelitemi] \textbf{\textit{iprover\_eq}:} iProver-Eq is an
+instantiation-based prover with native support for equality developed by
+Konstantin Korovin and Christoph Sticksel \cite{korovin-sticksel-2010}. To use
+iProver-Eq, set the environment variable \texttt{IPROVER\_EQ\_HOME} to the
+directory that contains the \texttt{iprover-eq} executable. Sledgehammer has
+been tested with version 0.8.
+
\item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic
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
@@ -920,6 +934,7 @@
requires version 4.0 or above. To use it, set the environment variable
\texttt{Z3\_HOME} to the directory that contains the \texttt{z3} executable.
\end{enum}
+\end{sloppy}
The following remote provers are supported:
@@ -940,14 +955,11 @@
servers. This ATP supports the TPTP typed first-order format (TFF0). The
remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.
-\item[\labelitemi] \textbf{\textit{remote\_iprover}:} iProver is a pure
-instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. The
+\item[\labelitemi] \textbf{\textit{remote\_iprover}:} The
remote version of iProver runs on Geoff Sutcliffe's Miami servers
\cite{sutcliffe-2000}.
-\item[\labelitemi] \textbf{\textit{remote\_iprover\_eq}:} iProver-Eq is an
-instantiation-based prover with native support for equality developed by
-Konstantin Korovin and Christoph Sticksel \cite{korovin-sticksel-2010}. The
+\item[\labelitemi] \textbf{\textit{remote\_iprover\_eq}:} The
remote version of iProver-Eq runs on Geoff Sutcliffe's Miami servers
\cite{sutcliffe-2000}.