# HG changeset patch
# User blanchet
# Date 1306188093 -7200
# Node ID bf45fd2488a2760cd44b54d579325dd0d38300cd
# Parent  5725deb11ae73f7749f7687d839142705bcb3f98
document primitive support for LEO-II and Satallax

diff -r 5725deb11ae7 -r bf45fd2488a2 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Tue May 24 00:01:33 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue May 24 00:01:33 2011 +0200
@@ -77,10 +77,11 @@
 \section{Introduction}
 \label{introduction}
 
-Sledgehammer is a tool that applies first-order automatic theorem provers (ATPs)
+Sledgehammer is a tool that applies automatic theorem provers (ATPs)
 and satisfiability-modulo-theories (SMT) solvers on the current goal. The
-supported ATPs are E \cite{schulz-2002}, SInE-E \cite{sine}, SNARK \cite{snark},
-SPASS \cite{weidenbach-et-al-2009}, ToFoF-E \cite{tofof}, Vampire
+supported ATPs are E \cite{schulz-2002}, LEO-II \cite{leo2}, Satallax
+\cite{satallax}, SInE-E \cite{sine}, SNARK \cite{snark}, SPASS
+\cite{weidenbach-et-al-2009}, ToFoF-E \cite{tofof}, Vampire
 \cite{riazanov-voronkov-2002}, and Waldmeister \cite{waldmeister}. The ATPs are
 run either locally or remotely via the System\-On\-TPTP web service
 \cite{sutcliffe-2000}. In addition to the ATPs, the SMT solvers Z3 \cite{z3} is
@@ -135,8 +136,8 @@
 \subsection{Installing ATPs}
 
 Currently, E, SPASS, and Vampire can be run locally; in addition, E, Vampire,
-SInE-E, SNARK, ToFoF-E, and Waldmeister are available remotely via
-System\-On\-TPTP \cite{sutcliffe-2000}. If you want better performance, you
+LEO-II, Satallax, SInE-E, SNARK, ToFoF-E, and Waldmeister are available remotely
+via System\-On\-TPTP \cite{sutcliffe-2000}. If you want better performance, you
 should at least install E and SPASS locally.
 
 There are three main ways to install ATPs on your machine:
@@ -261,12 +262,12 @@
 To minimize the number of lemmas, try this: \\
 \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}]~(\textit{list.inject}). \\[3\smallskipamount]
 %
-Sledgehammer: ``\textit{remote\_waldmeister}'' for subgoal 1: \\
-$[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this command: \textbf{by} (\textit{metis hd.simps insert\_Nil}). \\
-To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_waldmeister}] \\
-\phantom{\textbf{sledgehammer}~}(\textit{hd.simps insert\_Nil}). \\[3\smallskipamount]
+%Sledgehammer: ``\textit{remote\_waldmeister}'' for subgoal 1: \\
+%$[a] = [b] \,\Longrightarrow\, a = b$ \\
+%Try this command: \textbf{by} (\textit{metis hd.simps insert\_Nil}). \\
+%To minimize the number of lemmas, try this: \\
+%\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_waldmeister}] \\
+%\phantom{\textbf{sledgehammer}~}(\textit{hd.simps insert\_Nil}). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{remote\_sine\_e}'' for subgoal 1: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
@@ -281,11 +282,13 @@
 \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_z3}]~(\textit{hd.simps}).
 \postw
 
-Sledgehammer ran E, SInE-E, SPASS, Vampire, Waldmeister, and Z3 in parallel.
+Sledgehammer ran E, SInE-E, SPASS, Vampire, %Waldmeister,
+and Z3 in parallel.
 Depending on which provers are installed and how many processor cores are
 available, some of the provers might be missing or present with a
-\textit{remote\_} prefix. Waldmeister is run only for unit equational problems,
-where the goal's conclusion is a (universally quantified) equation.
+\textit{remote\_} prefix.
+%Waldmeister is run only for unit equational problems,
+%where the goal's conclusion is a (universally quantified) equation.
 
 For each successful prover, Sledgehammer gives a one-liner proof that uses the
 \textit{metis} or \textit{smt} method. You can click the proof to insert it into
@@ -672,29 +675,29 @@
 executable, including the file name. Sledgehammer has been tested with version
 2.2.
 
-\item[$\bullet$] \textbf{\textit{e}:} E is an ATP developed by Stephan Schulz
-\cite{schulz-2002}. To use E, set the environment variable
-\texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable,
-or install the prebuilt E package from Isabelle's download page. See
+\item[$\bullet$] \textbf{\textit{e}:} E is a first-order resolution prover
+developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment
+variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}
+executable, or install the prebuilt E package from Isabelle's download page. See
 \S\ref{installation} for details.
 
-\item[$\bullet$] \textbf{\textit{spass}:} SPASS is an ATP developed by Christoph
-Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the
-environment variable \texttt{SPASS\_HOME} to the directory that contains the
-\texttt{SPASS} executable, or install the prebuilt SPASS package from Isabelle's
-download page. Sledgehammer requires version 3.5 or above. See
-\S\ref{installation} for details.
+\item[$\bullet$] \textbf{\textit{spass}:} SPASS is a first-order resolution
+prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
+To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
+that contains the \texttt{SPASS} executable, or install the prebuilt SPASS
+package from Isabelle's download page. Sledgehammer requires version 3.5 or
+above. See \S\ref{installation} for details.
 
 \item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
 SRI \cite{yices}. To use Yices, set the environment variable
 \texttt{YICES\_SOLVER} to the complete path of the executable, including the
 file name. Sledgehammer has been tested with version 1.0.
 
-\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP 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. Sledgehammer has been tested with
-versions 11, 0.6, and 1.0.
+\item[$\bullet$] \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. Sledgehammer has been tested with versions 11, 0.6, and 1.0.
 
 \item[$\bullet$] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
 Microsoft Research \cite{z3}. To use Z3, set the environment variable
@@ -717,13 +720,23 @@
 \item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs
 on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
 
+\item[$\bullet$] \textbf{\textit{remote\_leo2}:} LEO-II is an automatic
+higher-order prover developed by Christoph Benzm\"uller et al. \cite{leo2}. The
+remote version of LEO-II runs on Geoff Sutcliffe's Miami servers. In the current
+setup, the problems given to LEO-II are only mildly higher-order.
+
+\item[$\bullet$] \textbf{\textit{remote\_satallax}:} Satallax is an automatic
+higher-order prover developed by Chad Brown et al. \cite{satallax}. The remote
+version of Satallax runs on Geoff Sutcliffe's Miami servers. In the current
+setup, the problems given to Satallax are only mildly higher-order.
+
 \item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
 developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
 SInE runs on Geoff Sutcliffe's Miami servers.
 
-\item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a prover
-developed by Stickel et al.\ \cite{snark}. The remote version of
-SNARK runs on Geoff Sutcliffe's Miami servers.
+\item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a first-order
+resolution prover developed by Stickel et al.\ \cite{snark}. The remote version
+of SNARK runs on Geoff Sutcliffe's Miami servers.
 
 \item[$\bullet$] \textbf{\textit{remote\_tofof\_e}:} ToFoF-E is a metaprover
 developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
@@ -755,9 +768,9 @@
 in Proof General.
 
 It is a good idea to run several provers in parallel, although it could slow
-down your machine. Running E, SPASS, Vampire, and SInE-E together for 5 seconds
-yields a better success rate than running the most effective of these (Vampire)
-for 120 seconds \cite{boehme-nipkow-2010}.
+down your machine. Running E, SPASS, and Vampire for 5~seconds yields a similar
+success rate to running the most effective of these for 120~seconds
+\cite{boehme-nipkow-2010}.
 
 \opnodefault{prover}{string}
 Alias for \textit{provers}.
@@ -871,8 +884,8 @@
 $\mathit{type\_info\_}\tau(t)$.
 
 \item[$\bullet$] \textbf{\textit{simple} (sound):} Use the prover's support for
-simply typed first-order logic if available; otherwise, fall back on
-\textit{mangled\_preds}. The problem is monomorphized.
+simple types if available; otherwise, fall back on \textit{mangled\_preds}. The
+problem is monomorphized.
 
 \item[$\bullet$]
 \textbf{%
diff -r 5725deb11ae7 -r bf45fd2488a2 doc-src/manual.bib
--- a/doc-src/manual.bib	Tue May 24 00:01:33 2011 +0200
+++ b/doc-src/manual.bib	Tue May 24 00:01:33 2011 +0200
@@ -140,6 +140,17 @@
 
 %B
 
+@inproceedings{satallax,
+  title = "Analytic Tableaux for Higher-Order Logic with Choice",
+  author = "Julian Backes and Chad E. Brown",
+  booktitle={Automated Reasoning: IJCAR 2010},
+  editor={J. Giesl and R. H\"ahnle},
+  publisher = Springer,
+  series = LNCS,
+  volume = 6173,
+  pages = "76--90",
+  year = 2010}
+
 @book{Baader-Nipkow,author={Franz Baader and Tobias Nipkow},
 title="Term Rewriting and All That",publisher=CUP,year=1998}
 
@@ -204,6 +215,17 @@
   title =        {Calculational reasoning revisited --- an {Isabelle/Isar} experience},
   crossref =     {tphols2001}}
 
+@inproceedings{leo2,
+  author = "Christoph Benzm{\"u}ller and Lawrence C. Paulson and Frank Theiss and Arnaud Fietzke",
+  title = "{LEO-II}---A Cooperative Automatic Theorem Prover for Higher-Order Logic",
+  editor = "Alessandro Armando and Peter Baumgartner and Gilles Dowek",
+  booktitle = "Automated Reasoning: IJCAR 2008",
+  publisher = Springer,
+  series = LNCS,
+  volume = 5195,
+  pages = "162--170",
+  year = 2008}
+
 @inProceedings{Berghofer-Bulwahn-Haftmann:2009:TPHOL,
     author = {Berghofer, Stefan and Bulwahn, Lukas and Haftmann, Florian},
     booktitle = {Theorem Proving in Higher Order Logics},
@@ -286,6 +308,8 @@
   editor={J. Giesl and R. H\"ahnle},
   publisher=Springer,
   series=LNCS,
+  volume = 6173,
+  pages = "107--121",
   year=2010}
 
 @Article{boyer86,