--- a/src/Doc/Sledgehammer/document/root.tex Fri Oct 25 14:47:42 2019 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Oct 25 14:51:16 2019 +0200
@@ -103,14 +103,13 @@
%
The supported ATPs are AgsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E
\cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF \cite{tofof}, iProver
-\cite{korovin-2009}, iProver-Eq \cite{korovin-sticksel-2010}, LEO-II
-\cite{leo2}, Leo-III \cite{leo3}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS
-\cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002},
-Waldmeister \cite{waldmeister}, and Zipperposition \cite{cruanes-2014}.
-The ATPs are run either locally or remotely via the System\-On\-TPTP web service
-\cite{sutcliffe-2000}. The supported SMT solvers are CVC3 \cite{cvc3}, CVC4
-\cite{cvc4}, veriT \cite{bouton-et-al-2009}, and Z3 \cite{z3}. These are always
-run locally.
+\cite{korovin-2009}, LEO-II \cite{leo2}, Leo-III \cite{leo3}, Satallax
+\cite{satallax}, SNARK \cite{snark}, SPASS \cite{weidenbach-et-al-2009},
+Vampire \cite{riazanov-voronkov-2002}, Waldmeister \cite{waldmeister}, and
+Zipperposition \cite{cruanes-2014}. The ATPs are run either locally or
+remotely via the System\-On\-TPTP web service \cite{sutcliffe-2000}. The
+supported SMT solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, veriT
+\cite{bouton-et-al-2009}, and Z3 \cite{z3}. These are always run locally.
The problem passed to the external provers (or solvers) consists of your current
goal together with a heuristic selection of hundreds of facts (theorems) from the
@@ -149,7 +148,7 @@
Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, Vampire, and
Zipperposition can be run locally; in addition, AgsyHOL, E, E-SInE, E-ToFoF,
-iProver, iProver-Eq, LEO-II, Leo-III, Satallax, SNARK, Vampire, and Waldmeister are
+iProver, LEO-II, Leo-III, Satallax, SNARK, Vampire, and Waldmeister are
available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers
CVC3, CVC4, veriT, and Z3 can be run locally.
@@ -789,13 +788,6 @@
executable. Sledgehammer has been tested with version 2.8. iProver depends on
E to clausify problems, so make sure that E is installed as well.
-\item[\labelitemi] \textbf{\textit{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}. To use
-iProver-Eq, set the environment variable \texttt{IPROVER\_EQ\_HOME} to the
-directory that contains the \texttt{iprover-eq} and \texttt{vclausify\_rel}
-executables. Sledgehammer has been tested with version 0.8.
-
\item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic
higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
with support for the TPTP typed higher-order syntax (THF0). To use LEO-II, set
@@ -880,10 +872,6 @@
remote version of iProver runs on Geoff Sutcliffe's Miami servers
\cite{sutcliffe-2000}.
-\item[\labelitemi] \textbf{\textit{remote\_iprover\_eq}:} The
-remote version of iProver-Eq runs on Geoff Sutcliffe's Miami servers
-\cite{sutcliffe-2000}.
-
\item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
--- a/src/HOL/Tools/ATP/atp_proof.ML Fri Oct 25 14:47:42 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Oct 25 14:51:16 2019 +0200
@@ -56,7 +56,6 @@
val e_tofofN : string
val ehohN : string
val iproverN : string
- val iprover_eqN : string
val leo2N : string
val leo3N : string
val pirateN : string
@@ -126,7 +125,6 @@
val e_tofofN = "e_tofof"
val ehohN = "ehoh"
val iproverN = "iprover"
-val iprover_eqN = "iprover_eq"
val leo2N = "leo2"
val leo3N = "leo3"
val pirateN = "pirate"
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 25 14:47:42 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 25 14:51:16 2019 +0200
@@ -394,21 +394,6 @@
val iprover = (iproverN, fn () => iprover_config)
-(* iProver-Eq *)
-
-val iprover_eq_config : atp_config =
- {exec = K (["IPROVER_EQ_HOME"], ["iprover-eq"]),
- arguments = #arguments iprover_config,
- proof_delims = #proof_delims iprover_config,
- known_failures = #known_failures iprover_config,
- prem_role = #prem_role iprover_config,
- best_slices = #best_slices iprover_config,
- best_max_mono_iters = #best_max_mono_iters iprover_config,
- best_max_new_mono_instances = #best_max_new_mono_instances iprover_config}
-
-val iprover_eq = (iprover_eqN, fn () => iprover_eq_config)
-
-
(* LEO-II *)
val leo2_config : atp_config =
@@ -733,9 +718,6 @@
val remote_iprover =
remotify_atp iprover "iProver" ["0.99"]
(K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
-val remote_iprover_eq =
- remotify_atp iprover_eq "iProver-Eq" ["0.8"]
- (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
val remote_leo2 =
remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"]
(K (((40, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *))
@@ -791,10 +773,9 @@
end
val atps =
- [agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, iprover_eq, leo2, leo3, satallax, spass,
- vampire, z3_tptp, zipperposition, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof,
- remote_iprover, remote_iprover_eq, remote_leo2, remote_leo3, remote_vampire, remote_snark,
- remote_pirate, remote_waldmeister]
+ [agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, leo2, leo3, satallax, spass, vampire,
+ z3_tptp, zipperposition, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof, remote_iprover,
+ remote_leo2, remote_leo3, remote_vampire, remote_snark, remote_pirate, remote_waldmeister]
val _ = Theory.setup (fold add_atp atps)