# HG changeset patch # User blanchet # Date 1572005162 -7200 # Node ID 1019b860955274b8fbb5ba24123230af549c9f05 # Parent 9b69bb9c1c8d140bc416667b9be733f10f3838bb removed support for remote Satallax because its output does not clearly identify the lemmas used diff -r 9b69bb9c1c8d -r 1019b8609552 src/Doc/Sledgehammer/document/root.tex --- 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 diff -r 9b69bb9c1c8d -r 1019b8609552 src/HOL/Tools/ATP/atp_satallax.ML --- 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 diff -r 9b69bb9c1c8d -r 1019b8609552 src/HOL/Tools/ATP/atp_systems.ML --- 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)