# HG changeset patch
# User blanchet
# Date 1306068664 -7200
# Node ID f838586ebec29cc48fc7d367f57d0ad0e72f3420
# Parent  0134d6650092f9e02141c1b4c62b9605d5a50927
document Waldmeister

diff -r 0134d6650092 -r f838586ebec2 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Sun May 22 14:51:01 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Sun May 22 14:51:04 2011 +0200
@@ -80,12 +80,12 @@
 Sledgehammer is a tool that applies first-order automatic theorem provers (ATPs)
 and satisfiability-modulo-theories (SMT) solvers on the current goal. The
 supported ATPs are E \cite{schulz-2002}, SPASS \cite{weidenbach-et-al-2009},
-Vampire \cite{riazanov-voronkov-2002}, SInE-E \cite{sine}, SNARK
-\cite{snark}, and ToFoF-E \cite{tofof}. 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 used by default, and you can tell
-Sledgehammer to try Yices \cite{yices} and CVC3 \cite{cvc3} as well; these
-are run either locally or on a server in Munich.
+Vampire \cite{riazanov-voronkov-2002}, SInE-E \cite{sine}, SNARK \cite{snark},
+ToFoF-E \cite{tofof}, 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
+used by default, and you can tell Sledgehammer to try Yices \cite{yices} and
+CVC3 \cite{cvc3} as well; these are run either locally or on a server in Munich.
 
 The problem passed to the automatic provers consists of your current goal
 together with a heuristic selection of hundreds of facts (theorems) from the
@@ -134,9 +134,9 @@
 \subsection{Installing ATPs}
 
 Currently, E, SPASS, and Vampire can be run locally; in addition, E, Vampire,
-SInE-E, SNARK, and ToFoF-E are available remotely via System\-On\-TPTP
-\cite{sutcliffe-2000}. If you want better performance, you should at least
-install E and SPASS locally.
+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:
 
@@ -708,6 +708,10 @@
 developed by Stickel et al.\ \cite{snark}. The remote version of
 SNARK runs on Geoff Sutcliffe's Miami servers.
 
+\item[$\bullet$] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit
+equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. The remote
+version of Waldmeister runs on Geoff Sutcliffe's Miami servers.
+
 \item[$\bullet$] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
 on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
 point).
diff -r 0134d6650092 -r f838586ebec2 doc-src/manual.bib
--- a/doc-src/manual.bib	Sun May 22 14:51:01 2011 +0200
+++ b/doc-src/manual.bib	Sun May 22 14:51:04 2011 +0200
@@ -624,6 +624,15 @@
   publisher	= {Wiley},
   year		= 1990}
 
+@article{waldmeister,
+  author = {Thomas Hillenbrand and Arnim Buch and Rolan Vogt and Bernd L\"ochner},
+  title = "Waldmeister: High-Performance Equational Deduction",
+  journal = JAR,
+  volume	= 18,
+  number	= 2,
+  pages		= {265--270},
+  year		= 1997}
+
 @book{HopcroftUllman,author={John E. Hopcroft and Jeffrey D. Ullman},
 title={Introduction to Automata Theory, Languages, and Computation.},
 publisher={Addison-Wesley},year=1979}