removed support for remote Satallax because its output does not clearly identify the lemmas used
--- a/src/Doc/Sledgehammer/document/root.tex Fri Oct 25 13:25:30 2019 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Oct 25 14:06:02 2019 +0200
@@ -893,9 +893,6 @@
highly experimental first-order resolution prover developed by Daniel Wand.
The remote version of Pirate run on a private server he generously set up.
-\item[\labelitemi] \textbf{\textit{remote\_satallax}:} The remote version of
-Satallax 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}. It supports the
TPTP typed first-order format (TFF0). The remote version of SNARK runs on
--- a/src/HOL/Tools/ATP/atp_satallax.ML Fri Oct 25 13:25:30 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_satallax.ML Fri Oct 25 14:06:02 2019 +0200
@@ -124,6 +124,7 @@
else
raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction")
end
+
fun to_satallax_step (((id, role), formula), (SOME (_,((rule, l), used_rules)))) =
let
val (used_assumptions, new_goals, generated_assumptions) = seperate_dependices used_rules
@@ -220,7 +221,7 @@
Linear_Part {node = node, succs = []}
else
let
- (*one singel goal is created, two hypothesis can be created, for the "and" rule:
+ (*one single goal is created, two hypothesis can be created, for the "and" rule:
(A /\ B) create two hypotheses A, and B.*)
fun set_hypotheses_as_goal [hypothesis] succs =
Linear_Part {node = add_detailled_eigen detailed_eigen
@@ -361,7 +362,7 @@
let
val role' = role_of_tptp_string role
val new_transformed = filter
- (fn s => size s >=4 andalso not (is_special_satallax_rule s) andalso not
+ (fn s => size s >= 4 andalso not (is_special_satallax_rule s) andalso not
(member (op =) already_transformed s)) used_assumptions
in
(map create_fact_step new_transformed
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 25 13:25:30 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 25 14:06:02 2019 +0200
@@ -783,9 +783,6 @@
val remote_leo3 =
remotify_atp leo3 "Leo-III" ["1.1"]
(K (((150, ""), leo3_thf1, "poly_native_higher", keep_lamsN, false), "") (* FUDGE *))
-val remote_satallax =
- remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
- (K (((150, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
val remote_vampire =
remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"]
(K (((400, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *))
@@ -839,8 +836,7 @@
[agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, iprover_eq, leo2, leo3, satallax, spass,
vampire, z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e,
remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_leo3,
- remote_satallax, remote_vampire, remote_snark, remote_pirate, remote_waldmeister,
- remote_waldmeister_new]
+ remote_vampire, remote_snark, remote_pirate, remote_waldmeister, remote_waldmeister_new]
val _ = Theory.setup (fold add_atp atps)