--- a/doc-src/Sledgehammer/sledgehammer.tex Fri Nov 04 17:19:33 2011 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Fri Nov 04 17:34:51 2011 +0100
@@ -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 17:19:33 2011 +0100
+++ b/doc-src/manual.bib Fri Nov 04 17:34:51 2011 +0100
@@ -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 17:19:33 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Nov 04 17:34:51 2011 +0100
@@ -40,6 +40,8 @@
val eN : string
val e_sineN : string
val e_tofofN : string
+ val iproverN : string
+ val iprover_eqN : string
val leo2N : string
val pffN : string
val phfN : string
@@ -125,6 +127,8 @@
val eN = "e"
val e_sineN = "e_sine"
val e_tofofN = "e_tofof"
+val iproverN = "iprover"
+val iprover_eqN = "iprover_eq"
val leo2N = "leo2"
val pffN = "pff"
val phfN = "phf"
@@ -528,6 +532,12 @@
val remote_e_sine =
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
Conjecture (K (500, FOF, "mono_guards??") (* FUDGE *))
+val remote_iprover =
+ remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
+ (K (150, FOF, "mono_guards??") (* FUDGE *))
+val remote_iprover_eq =
+ remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture
+ (K (150, FOF, "mono_guards??") (* FUDGE *))
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
[("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
@@ -565,8 +575,9 @@
val atps =
[e, leo2, pff, phf, satallax, spass, spass_new, vampire, z3_tptp, remote_e,
- remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine,
- 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;