# HG changeset patch
# User blanchet
# Date 1343895029 -7200
# Node ID 15f0cf52deea57e6ffd01d61d8f726a8ed162f6c
# Parent  fb461f81e76e73692e8d4e5c5e00752d96212564
document E-MaLeS

diff -r fb461f81e76e -r 15f0cf52deea doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu Aug 02 10:10:29 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu Aug 02 10:10:29 2012 +0200
@@ -203,10 +203,10 @@
 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
 \texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable.
 Sledgehammer has been tested with E 1.0 to 1.4, LEO-II 1.3.4, Satallax 2.2, 2.3,
-and 2.4, SPASS 3.8ds, and Vampire 0.6, 1.0, and 1.8.%
+and 2.4, SPASS 3.8ds, and Vampire 0.6 to 2.6.%
 \footnote{Following the rewrite of Vampire, the counter for version numbers was
-reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent
-than 9.0 or 11.5.}%
+reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, and 2.6 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},
@@ -859,7 +859,13 @@
 variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}
 executable and \texttt{E\_VERSION} to the version number (e.g., ``1.4''), or
 install the prebuilt E package from \download. Sledgehammer has been tested with
-versions 1.0 to 1.4.
+versions 1.0 to 1.6.
+
+\item[\labelitemi] \textbf{\textit{e\_males}:} E-MaLeS is a metaprover developed
+by Daniel K\"uhlwein that implements strategy scheduling on top of E. To use
+E-MaLeS, set the environment variable \texttt{E\_MALES\_HOME} to the directory
+that contains the \texttt{emales.py} script. Sledgehammer has been tested with
+version 1.1.
 
 \item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic
 higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
@@ -867,7 +873,7 @@
 the environment variable \texttt{LEO2\_HOME} to the directory that contains the
 \texttt{leo} executable. Sledgehammer requires version 1.2.9 or above.
 
-\item[\labelitemi] \textbf{\textit{metis}:} Although it is much less powerful than
+\item[\labelitemi] \textbf{\textit{metis}:} Although it is less powerful than
 the external provers, Metis itself can be used for proof search.
 
 \item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic
@@ -877,7 +883,8 @@
 \texttt{satallax} executable. Sledgehammer requires version 2.2 or above.
 
 \item[\labelitemi] \textbf{\textit{smt}:} The \textit{smt} proof method with the
-current settings (usually:\ Z3 with proof reconstruction).
+current settings (usually:\ Z3 with proof reconstruction) can be used for proof
+search.
 
 \item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution
 prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
@@ -886,14 +893,14 @@
 version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from
 \download. Sledgehammer requires version 3.8ds or above.
 
-\item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution
-prover developed by Andrei Voronkov and his colleagues
+\item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order
+resolution prover developed by Andrei Voronkov and his colleagues
 \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable
 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
 executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g.,
-``1.8rev1435''). Sledgehammer has been tested with versions 0.6, 1.0, and 1.8.
-Versions strictly above 1.8 (e.g., ``1.8rev1435'') support the TPTP typed
-first-order format (TFF0).
+``1.8rev1435'', ``2.6''). Sledgehammer has been tested with versions 0.6, 1.0,
+and 1.8. Versions strictly above 1.8 (e.g., ``1.8rev1435'') support the TPTP
+typed first-order format (TFF0).
 
 \item[\labelitemi] \textbf{\textit{yices}:} Yices is an SMT solver developed at
 SRI \cite{yices}. To use Yices, set the environment variable
@@ -911,8 +918,7 @@
 an ATP, exploiting Z3's support for the TPTP untyped and typed first-order
 formats (FOF and TFF0). It is included for experimental purposes. Sledgehammer
 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.
+\texttt{Z3\_HOME} to the directory that contains the \texttt{z3} executable.
 \end{enum}
 
 The following remote provers are supported: