--- a/src/Doc/Sledgehammer/document/root.tex Thu Oct 08 17:47:35 2020 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Oct 08 17:55:17 2020 +0200
@@ -102,23 +102,22 @@
\footnote{The distinction between ATPs and SMT solvers is convenient but mostly
historical.}
%
-The supported ATPs are agsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E
+The supported ATPs include agsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E
\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.
+\cite{leo3}, Satallax \cite{satallax}, 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
current theory context, filtered by relevance.
-The result of a successful proof search is some source text that usually (but
-not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed
-proof typically relies on the general-purpose \textit{metis} proof method, which
+The result of a successful proof search is some source text that typically
+reconstructs the proof within Isabelle. For ATPs, the reconstructed proof
+typically relies on the general-purpose \textit{metis} proof method, which
integrates the Metis ATP in Isabelle/HOL with explicit inferences going through
the kernel. Thus its results are correct by construction.
@@ -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,
-Alt-Ergo, E, iProver, LEO-II, Leo-III, Satallax, SNARK, Vampire, Waldmeister,
+Alt-Ergo, E, iProver, LEO-II, Leo-III, Satallax, Vampire, Waldmeister,
and Zipperposition are available remotely via System\-On\-TPTP
\cite{sutcliffe-2000}. The SMT solvers CVC3, CVC4, veriT, and Z3 can be run
locally.
@@ -765,14 +764,6 @@
install the prebuilt E package from \download. Sledgehammer has been tested with
versions 1.6 to 1.8.
-\item[\labelitemi] \textbf{\textit{e\_par}:} E-Par is an experimental metaprover
-developed by Josef Urban that implements strategy scheduling on top of E. To use
-E-Par, set the environment variable \texttt{E\_HOME} to the directory that
-contains the \texttt{runepar.pl} script and the \texttt{eprover} and
-\texttt{epclextract} executables, or use the prebuilt E package from \download.
-Be aware that E-Par is experimental software. It has been known to generate
-zombie processes. Use at your own risks.
-
\item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure
instantiation-based prover developed by Konstantin Korovin
\cite{korovin-2009}. To use iProver, set the environment variable
@@ -865,10 +856,6 @@
\item[\labelitemi] \textbf{\textit{remote\_leo3}:} The remote version of Leo-III
runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
-\item[\labelitemi] \textbf{\textit{remote\_snark}:} SNARK is a first-order
-resolution prover developed by Stickel et al.\ \cite{snark}. The remote
-version of SNARK runs on Geoff Sutcliffe's Miami servers.
-
\item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of
Vampire runs on Geoff Sutcliffe's Miami servers.
--- a/src/HOL/Sledgehammer.thy Thu Oct 08 17:47:35 2020 +0200
+++ b/src/HOL/Sledgehammer.thy Thu Oct 08 17:55:17 2020 +0200
@@ -13,9 +13,6 @@
"sledgehammer_params" :: thy_decl
begin
-lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
- by (erule contrapos_nn) (rule arg_cong)
-
ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Oct 08 17:47:35 2020 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Oct 08 17:55:17 2020 +0200
@@ -44,17 +44,14 @@
type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list
- (* Named ATPs *)
val agsyholN : string
val alt_ergoN : string
val eN : string
- val e_parN : string
val iproverN : string
val leo2N : string
val leo3N : string
val pirateN : string
val satallaxN : string
- val snarkN : string
val spassN : string
val vampireN : string
val waldmeisterN : string
@@ -109,18 +106,14 @@
open ATP_Util
open ATP_Problem
-(* Named ATPs *)
-
val agsyholN = "agsyhol"
val alt_ergoN = "alt_ergo"
val eN = "e"
-val e_parN = "e_par"
val iproverN = "iprover"
val leo2N = "leo2"
val leo3N = "leo3"
val pirateN = "pirate"
val satallaxN = "satallax"
-val snarkN = "snark"
val spassN = "spass"
val vampireN = "vampire"
val waldmeisterN = "waldmeister"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Oct 08 17:47:35 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Oct 08 17:55:17 2020 +0200
@@ -315,27 +315,6 @@
val e = (eN, fn () => e_config)
-(* E-Par *)
-
-val e_par_config : atp_config =
- {exec = K (["E_HOME"], ["runepar.pl"]),
- arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
- string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^ " 2" (* proofs *),
- proof_delims = tstp_proof_delims,
- known_failures = #known_failures e_config,
- prem_role = Conjecture,
- best_slices =
- (* FUDGE *)
- K [(0.25, (((500, meshN), FOF, "mono_guards??", combs_or_liftingN, false), "")),
- (0.25, (((150, meshN), FOF, "poly_tags??", combs_or_liftingN, false), "")),
- (0.25, (((50, meshN), FOF, "mono_tags??", combs_or_liftingN, false), "")),
- (0.25, (((1000, meshN), FOF, "poly_guards??", combsN, false), ""))],
- best_max_mono_iters = default_max_mono_iters,
- best_max_new_mono_instances = default_max_new_mono_instances}
-
-val e_par = (e_parN, fn () => e_par_config)
-
-
(* iProver *)
val iprover_config : atp_config =
@@ -673,10 +652,6 @@
val remote_leo3 =
remotify_atp leo3 "Leo-III" ["1.1"]
(K (((150, ""), THF (Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *))
-val remote_snark =
- remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"]
- [("refutation.", "end_refutation.")] [] Hypothesis
- (K (((100, ""), TFF Monomorphic, "mono_native", liftingN, false), "") (* FUDGE *))
val remote_vampire =
remotify_atp vampire "Vampire" ["THF-4.4"]
(K (((400, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), remote_vampire_command) (* FUDGE *))
@@ -719,9 +694,9 @@
end
val atps =
- [agsyhol, alt_ergo, e, e_par, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp,
- zipperposition, remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2,
- remote_leo3, remote_snark, remote_vampire, remote_waldmeister, remote_zipperposition]
+ [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition,
+ remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3,
+ remote_vampire, remote_waldmeister, remote_zipperposition]
val _ = Theory.setup (fold add_atp atps)