src/HOL/Tools/res_atp_methods.ML
author mengj
Fri Oct 28 02:28:20 2005 +0200 (2005-10-28)
changeset 18002 35ec4681d38f
parent 17907 c20e4bddcb11
child 18195 971dc7439088
permissions -rw-r--r--
Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals.
mengj@17905
     1
(* ID: $Id$
mengj@17907
     2
   Author: Jia Meng, NICTA
mengj@17905
     3
*)
mengj@17905
     4
mengj@17905
     5
mengj@17905
     6
structure ResAtpMethods =
mengj@17905
     7
mengj@17905
     8
struct
mengj@17905
     9
  
mengj@17905
    10
mengj@17905
    11
val vampire_time = ref 60;
mengj@17905
    12
val eprover_time = ref 60;
mengj@17905
    13
mengj@17905
    14
fun run_vampire time =  
mengj@17905
    15
    if (time >0) then vampire_time:= time
mengj@17905
    16
    else vampire_time:=60;
mengj@17905
    17
mengj@17905
    18
fun run_eprover time = 
mengj@17905
    19
    if (time > 0) then eprover_time:= time
mengj@17905
    20
    else eprover_time:=60;
mengj@17905
    21
mengj@17905
    22
fun vampireLimit () = !vampire_time;
mengj@17905
    23
fun eproverLimit () = !eprover_time;
mengj@17905
    24
mengj@17905
    25
mengj@17905
    26
mengj@17905
    27
(* convert the negated 1st subgoal into CNF, write to files and call an ATP oracle *)
mengj@18002
    28
fun res_atp_tac res_atp_oracle tptp_form make_nnf timeLimit ctxt files tfrees n thm =
mengj@17905
    29
    SELECT_GOAL
mengj@17905
    30
	((EVERY1 [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac, 
mengj@17905
    31
		  METAHYPS(fn negs =>
mengj@17905
    32
			      HEADGOAL(Tactic.rtac 
mengj@17905
    33
					   (res_atp_oracle (ProofContext.theory_of ctxt) 
mengj@18002
    34
							   ((tptp_form (make_clauses (map make_nnf negs)) n tfrees)::files, timeLimit))))]) handle Fail _ => no_tac) n thm;
mengj@17905
    35
mengj@18002
    36
(* vampire and eprover tactics *)
mengj@18002
    37
val vampireF_tac = res_atp_tac vampire_oracle ResAtpSetup.tptp_form make_nnf (!vampire_time);
mengj@17905
    38
mengj@18002
    39
val vampireH_tac = res_atp_tac vampire_oracle ResAtpSetup.tptp_formH make_nnf1 (!vampire_time);
mengj@17905
    40
mengj@18002
    41
val eproverF_tac = res_atp_tac eprover_oracle ResAtpSetup.tptp_form make_nnf (!eprover_time);
mengj@17905
    42
mengj@18002
    43
val eproverH_tac = res_atp_tac eprover_oracle ResAtpSetup.tptp_formH make_nnf1 (!eprover_time);
mengj@17905
    44
mengj@17905
    45
val ResAtps_setup = [Method.add_methods 
mengj@18002
    46
		 [("vampireF", ResAtpSetup.atp_method_F vampireF_tac, "A Vampire method for FOL problems"),
mengj@18002
    47
		   ("eproverF", ResAtpSetup.atp_method_F eproverF_tac, "A E prover method for FOL problems"),
mengj@18002
    48
			("vampireH",ResAtpSetup.atp_method_H vampireH_tac, "A Vampire method for HOL problems"),
mengj@18002
    49
				("eproverH",ResAtpSetup.atp_method_H eproverH_tac,"A E prover method for HOL problems")]];
mengj@17905
    50
mengj@17905
    51
mengj@17905
    52
mengj@17905
    53
mengj@17907
    54
end