removed support for E-ToFoF, which has lost its raison d'etre since E 2.0 supports TF0
--- a/src/Doc/Sledgehammer/document/root.tex Fri Oct 25 14:55:14 2019 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Oct 25 14:59:56 2019 +0200
@@ -102,14 +102,14 @@
historical.}
%
The supported ATPs are AgsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E
-\cite{schulz-2002}, E-ToFoF \cite{tofof}, iProver \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.
+\cite{schulz-2002}, iProver \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
@@ -859,11 +859,6 @@
\item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
-\item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover
-developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
-servers. This ATP supports the TPTP typed first-order format (TFF0). The
-remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.
-
\item[\labelitemi] \textbf{\textit{remote\_iprover}:} The
remote version of iProver runs on Geoff Sutcliffe's Miami servers
\cite{sutcliffe-2000}.
--- a/src/HOL/Tools/ATP/atp_proof.ML Fri Oct 25 14:55:14 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Oct 25 14:59:56 2019 +0200
@@ -52,7 +52,6 @@
val eN : string
val e_malesN : string
val e_parN : string
- val e_tofofN : string
val ehohN : string
val iproverN : string
val leo2N : string
@@ -120,7 +119,6 @@
val eN = "e"
val e_malesN = "e_males"
val e_parN = "e_par"
-val e_tofofN = "e_tofof"
val ehohN = "ehoh"
val iproverN = "iprover"
val leo2N = "leo2"
@@ -422,8 +420,6 @@
val waldmeister_conjecture_name = "conjecture_1"
-val tofof_fact_prefix = "fof_"
-
fun is_same_term subst tm1 tm2 =
let
fun do_term_pair (AAbs (((var1, typ1), body1), args1)) (AAbs (((var2, typ2), body2), args2))
@@ -573,7 +569,7 @@
if role' = Definition then
(((num, map fst (find_formula_in_problem phi problem)), phi), "", [])
else
- (((num, [s |> perhaps (try (unprefix tofof_fact_prefix))]), phi), "", [])
+ (((num, [s]), phi), "", [])
| Inference_Source (rule, deps) => (((num, []), phi), rule, deps))
in
[(name, role', phi, rule, map (rpair []) deps)]
@@ -603,8 +599,7 @@
phi |> not (is_same_formula false [] (mk_anot phi) phi') ? commute_eq)
| _ => ((num, []), phi))
else
- ((num, [s |> perhaps (try (unprefix tofof_fact_prefix))]),
- phi),
+ ((num, [s]), phi),
role, "", [])
| File_Source _ =>
(((num, map fst (find_formula_in_problem phi problem)), phi), role, "", [])
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 25 14:55:14 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 25 14:59:56 2019 +0200
@@ -731,9 +731,6 @@
remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"]
[("refutation.", "end_refutation.")] [] Hypothesis
(K (((100, ""), TFF Monomorphic, "mono_native", liftingN, false), "") (* FUDGE *))
-val remote_e_tofof =
- remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis
- (K (((150, ""), TFF Monomorphic, "mono_native", liftingN, false), "") (* FUDGE *))
val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??"
@@ -771,8 +768,8 @@
val atps =
[agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, leo2, leo3, satallax, spass, vampire,
- z3_tptp, zipperposition, remote_agsyhol, remote_e, remote_e_tofof, remote_iprover, remote_leo2,
- remote_leo3, remote_vampire, remote_snark, remote_pirate, remote_waldmeister]
+ z3_tptp, zipperposition, remote_agsyhol, remote_e, remote_iprover, remote_leo2, remote_leo3,
+ remote_vampire, remote_snark, remote_pirate, remote_waldmeister]
val _ = Theory.setup (fold add_atp atps)