--- 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}.
--- 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}},
--- 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;