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.
     1 (* ID: $Id$
     2    Author: Jia Meng, NICTA
     3 *)
     4 
     5 
     6 structure ResAtpMethods =
     7 
     8 struct
     9   
    10 
    11 val vampire_time = ref 60;
    12 val eprover_time = ref 60;
    13 
    14 fun run_vampire time =  
    15     if (time >0) then vampire_time:= time
    16     else vampire_time:=60;
    17 
    18 fun run_eprover time = 
    19     if (time > 0) then eprover_time:= time
    20     else eprover_time:=60;
    21 
    22 fun vampireLimit () = !vampire_time;
    23 fun eproverLimit () = !eprover_time;
    24 
    25 
    26 
    27 (* convert the negated 1st subgoal into CNF, write to files and call an ATP oracle *)
    28 fun res_atp_tac res_atp_oracle tptp_form make_nnf timeLimit ctxt files tfrees n thm =
    29     SELECT_GOAL
    30 	((EVERY1 [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac, 
    31 		  METAHYPS(fn negs =>
    32 			      HEADGOAL(Tactic.rtac 
    33 					   (res_atp_oracle (ProofContext.theory_of ctxt) 
    34 							   ((tptp_form (make_clauses (map make_nnf negs)) n tfrees)::files, timeLimit))))]) handle Fail _ => no_tac) n thm;
    35 
    36 (* vampire and eprover tactics *)
    37 val vampireF_tac = res_atp_tac vampire_oracle ResAtpSetup.tptp_form make_nnf (!vampire_time);
    38 
    39 val vampireH_tac = res_atp_tac vampire_oracle ResAtpSetup.tptp_formH make_nnf1 (!vampire_time);
    40 
    41 val eproverF_tac = res_atp_tac eprover_oracle ResAtpSetup.tptp_form make_nnf (!eprover_time);
    42 
    43 val eproverH_tac = res_atp_tac eprover_oracle ResAtpSetup.tptp_formH make_nnf1 (!eprover_time);
    44 
    45 val ResAtps_setup = [Method.add_methods 
    46 		 [("vampireF", ResAtpSetup.atp_method_F vampireF_tac, "A Vampire method for FOL problems"),
    47 		   ("eproverF", ResAtpSetup.atp_method_F eproverF_tac, "A E prover method for FOL problems"),
    48 			("vampireH",ResAtpSetup.atp_method_H vampireH_tac, "A Vampire method for HOL problems"),
    49 				("eproverH",ResAtpSetup.atp_method_H eproverH_tac,"A E prover method for HOL problems")]];
    50 
    51 
    52 
    53 
    54 end