# HG changeset patch
# User blanchet
# Date 1320419159 0
# Node ID 4f6ae54233117837fcff381bd6fce424125e8b12
# Parent  b9d5d3625e9a897460cd57a7d05a431f7f73131a
document new experimental provers

diff -r b9d5d3625e9a -r 4f6ae5423311 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Fri Nov 04 15:05:58 2011 +0000
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri Nov 04 15:05:59 2011 +0000
@@ -141,9 +141,10 @@
 \subsection{Installing ATPs}
 
 Currently, E, LEO-II, Satallax, SPASS, and Vampire can be run locally; in
-addition, E, E-SInE, E-ToFoF, LEO-II, Satallax, SNARK, Waldmeister, and Vampire
-are available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. If you want
-better performance, you should at least install E and SPASS locally.
+addition, E, E-SInE, E-ToFoF, iProver, iProver-Eq, LEO-II, Satallax, SNARK,
+Waldmeister, and Vampire 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:
 
@@ -792,6 +793,20 @@
 servers. This ATP supports the TPTP many-typed first-order format (TFF0). The
 remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.
 
+\item[$\bullet$] \textbf{\textit{remote\_iprover}:} iProver is a pure
+instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. The
+remote version of iProver runs on Geoff Sutcliffe's Miami servers
+\cite{sutcliffe-2000}.
+
+\item[$\bullet$] \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
+remote version of iProver-Eq runs on Geoff Sutcliffe's Miami servers
+\cite{sutcliffe-2000}.
+
+The remote version of LEO-II
+runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
+
 \item[$\bullet$] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
 runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
 
diff -r b9d5d3625e9a -r 4f6ae5423311 doc-src/manual.bib
--- a/doc-src/manual.bib	Fri Nov 04 15:05:58 2011 +0000
+++ b/doc-src/manual.bib	Fri Nov 04 15:05:59 2011 +0000
@@ -798,6 +798,30 @@
   volume	= 27,
   pages		= {97-109}}
 
+@inproceedings{korovin-2009,
+  title = "Instantiation-Based Automated Reasoning: From Theory to Practice",
+  author = "Konstantin Korovin",
+  editor = "Renate A. Schmidt",
+  booktitle = {Automated Deduction --- CADE-22},
+  series = "LNAI",
+  volume = {5663},
+  pages = "163--166",
+  year = 2009,
+  publisher = "Springer"}
+
+@inproceedings{korovin-sticksel-2010,
+  author    = {Konstantin Korovin and
+               Christoph Sticksel},
+  title     = {{iP}rover-{E}q: An Instantiation-Based Theorem Prover with Equality},
+  year      = {2010},
+  pages     = {196--202},
+  booktitle={Automated Reasoning: IJCAR 2010},
+  editor={J. Giesl and R. H\"ahnle},
+  publisher = Springer,
+  series = LNCS,
+  volume = 6173,
+  year = 2010}
+
 @InProceedings{krauss2006,
   author   =  {Alexander Krauss},
   title    =  {Partial Recursive Functions in {Higher-Order Logic}},
diff -r b9d5d3625e9a -r 4f6ae5423311 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Nov 04 15:05:58 2011 +0000
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Nov 04 15:05:59 2011 +0000
@@ -575,9 +575,9 @@
 
 val atps =
   [e, leo2, pff, phf, satallax, spass, spass_new, vampire, z3_tptp, remote_e,
-   remote_e_sine, remote_iprover, remote_iprover_eq, remote_leo2,
-   remote_satallax, remote_vampire, remote_z3_tptp, remote_snark,
-   remote_e_tofof, remote_waldmeister]
+   remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
+   remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark,
+   remote_waldmeister]
 val setup = fold add_atp atps
 
 end;