# HG changeset patch # User blanchet # Date 1282462990 -7200 # Node ID 979a0b37f981bd519fe47418f19c943845edd3b7 # Parent 2479d541bc6101b69694cf3d4c154adcafcdb72c prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible; the disjunctive view of "conjecture" is nonstandard but taken by E, SPASS, Vampire, etc. diff -r 2479d541bc61 -r 979a0b37f981 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Sun Aug 22 08:30:19 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Sun Aug 22 09:43:10 2010 +0200 @@ -22,7 +22,7 @@ val timestamp : unit -> string val is_tptp_variable : string -> bool val strings_for_tptp_problem : - (string * string problem_line list) list -> string list + bool -> (string * string problem_line list) list -> string list val nice_tptp_problem : bool -> ('a * (string * string) problem_line list) list -> ('a * string problem_line list) list @@ -48,6 +48,10 @@ val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now +fun string_for_kind Axiom = "axiom" + | string_for_kind Hypothesis = "hypothesis" + | string_for_kind Conjecture = "conjecture" + fun string_for_term (ATerm (s, [])) = s | string_for_term (ATerm ("equal", ts)) = space_implode " = " (map string_for_term ts) @@ -74,20 +78,26 @@ (map string_for_formula phis) ^ ")" | string_for_formula (AAtom tm) = string_for_term tm -fun string_for_problem_line (Fof (ident, kind, phi)) = - "fof(" ^ ident ^ ", " ^ - (case kind of - Axiom => "axiom" - | Hypothesis => "hypothesis" - | Conjecture => "conjecture") ^ - ",\n (" ^ string_for_formula phi ^ ")).\n" -fun strings_for_tptp_problem problem = +fun string_for_problem_line use_conjecture_for_hypotheses + (Fof (ident, kind, phi)) = + let + val (kind, phi) = + if kind = Hypothesis andalso use_conjecture_for_hypotheses then + (Conjecture, AConn (ANot, [phi])) + else + (kind, phi) + in + "fof(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^ + string_for_formula phi ^ ")).\n" + end +fun strings_for_tptp_problem use_conjecture_for_hypotheses problem = "% This file was generated by Isabelle (most likely Sledgehammer)\n\ \% " ^ timestamp () ^ "\n" :: maps (fn (_, []) => [] | (heading, lines) => "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" :: - map string_for_problem_line lines) problem + map (string_for_problem_line use_conjecture_for_hypotheses) lines) + problem fun is_tptp_variable s = Char.isUpper (String.sub (s, 0)) diff -r 2479d541bc61 -r 979a0b37f981 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sun Aug 22 08:30:19 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sun Aug 22 09:43:10 2010 +0200 @@ -20,7 +20,8 @@ known_failures: (failure * string) list, default_max_relevant_per_iter: int, default_theory_relevant: bool, - explicit_forall: bool} + explicit_forall: bool, + use_conjecture_for_hypotheses: bool} val string_for_failure : failure -> string val known_failure_in_output : @@ -51,7 +52,8 @@ known_failures: (failure * string) list, default_max_relevant_per_iter: int, default_theory_relevant: bool, - explicit_forall: bool} + explicit_forall: bool, + use_conjecture_for_hypotheses: bool} val missing_message_tail = " appears to be missing. You will need to install it if you want to run \ @@ -146,7 +148,8 @@ (OutOfResources, "SZS status ResourceOut")], default_max_relevant_per_iter = 50 (* FIXME *), default_theory_relevant = false, - explicit_forall = false} + explicit_forall = false, + use_conjecture_for_hypotheses = true} val e = ("e", e_config) @@ -173,7 +176,8 @@ (SpassTooOld, "tptp2dfg")], default_max_relevant_per_iter = 35 (* FIXME *), default_theory_relevant = true, - explicit_forall = true} + explicit_forall = true, + use_conjecture_for_hypotheses = true} val spass = ("spass", spass_config) @@ -199,7 +203,8 @@ (VampireTooOld, "not a valid option")], default_max_relevant_per_iter = 45 (* FIXME *), default_theory_relevant = false, - explicit_forall = false} + explicit_forall = false, + use_conjecture_for_hypotheses = true} val vampire = ("vampire", vampire_config) @@ -230,7 +235,8 @@ | SOME sys => sys); fun remote_config system_prefix proof_delims known_failures - default_max_relevant_per_iter default_theory_relevant = + default_max_relevant_per_iter default_theory_relevant + use_conjecture_for_hypotheses = {exec = ("ISABELLE_ATP", "scripts/remote_atp"), required_execs = [], arguments = fn _ => fn timeout => @@ -242,20 +248,25 @@ [(TimedOut, "says Timeout")], default_max_relevant_per_iter = default_max_relevant_per_iter, default_theory_relevant = default_theory_relevant, - explicit_forall = true} + explicit_forall = true, + use_conjecture_for_hypotheses = use_conjecture_for_hypotheses} fun remotify_config system_prefix ({proof_delims, known_failures, default_max_relevant_per_iter, - default_theory_relevant, ...} : prover_config) : prover_config = + default_theory_relevant, use_conjecture_for_hypotheses, ...} + : prover_config) : prover_config = remote_config system_prefix proof_delims known_failures default_max_relevant_per_iter default_theory_relevant + use_conjecture_for_hypotheses val remotify_name = prefix "remote_" fun remote_prover name system_prefix proof_delims known_failures - default_max_relevant_per_iter default_theory_relevant = + default_max_relevant_per_iter default_theory_relevant + use_conjecture_for_hypotheses = (remotify_name name, remote_config system_prefix proof_delims known_failures - default_max_relevant_per_iter default_theory_relevant) + default_max_relevant_per_iter default_theory_relevant + use_conjecture_for_hypotheses) fun remotify_prover (name, config) system_prefix = (remotify_name name, remotify_config system_prefix config) @@ -263,10 +274,10 @@ val remote_vampire = remotify_prover vampire "Vampire---9" val remote_sine_e = remote_prover "sine_e" "SInE---" [] - [(Unprovable, "says Unknown")] 150 (* FIXME *) false + [(Unprovable, "says Unknown")] 150 (* FIXME *) false true val remote_snark = remote_prover "snark" "SNARK---" [("refutation.", "end_refutation.")] [] - 50 (* FIXME *) false + 50 (* FIXME *) false true (* Setup *) diff -r 2479d541bc61 -r 979a0b37f981 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sun Aug 22 08:30:19 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sun Aug 22 09:43:10 2010 +0200 @@ -209,7 +209,7 @@ fun prover_fun atp_name {exec, required_execs, arguments, proof_delims, known_failures, default_max_relevant_per_iter, default_theory_relevant, - explicit_forall} + explicit_forall, use_conjecture_for_hypotheses} ({debug, verbose, overlord, full_types, explicit_apply, relevance_threshold, relevance_convergence, max_relevant_per_iter, theory_relevant, @@ -309,7 +309,9 @@ val (problem, pool, conjecture_offset, axiom_names) = prepare_problem ctxt readable_names explicit_forall full_types explicit_apply hyp_ts concl_t the_axioms - val _ = File.write_list probfile (strings_for_tptp_problem problem) + val ss = strings_for_tptp_problem use_conjecture_for_hypotheses + problem + val _ = File.write_list probfile ss val conjecture_shape = conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 |> map single