isabelle: src/HOL/Tools/res_atp_methods.ML@7706aeac6cf1 (annotated)

17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	1	(* ID: $Id$
17907 c20e4bddcb11 * empty log message * mengj parents: 17905 diff changeset	2	Author: Jia Meng, NICTA
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	3	*)
1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	4
1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	5
1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	6	structure ResAtpMethods =
1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	7
1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	8	struct
1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	9
19193 45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 19128 diff changeset	10	(* convert the negated 1st subgoal into CNF, write to file and call an ATP oracle *)
18271 0e9a851db989 Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs. mengj parents: 18195 diff changeset	11	fun res_atp_tac res_atp_oracle mode timeLimit ctxt user_thms n thm =
19193 45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 19128 diff changeset	12	(EVERY' [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac,
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	13	METAHYPS(fn negs =>
1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	14	HEADGOAL(Tactic.rtac
1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	15	(res_atp_oracle (ProofContext.theory_of ctxt)
19193 45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 19128 diff changeset	16	(ResAtp.write_subgoal_file mode ctxt negs user_thms n, timeLimit))))] n thm) handle (Fail _) => Seq.empty;
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	17
18002 35ec4681d38f 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 parents: 17907 diff changeset	18	(* vampire and eprover tactics *)
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	19
19193 45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 19128 diff changeset	20	fun vampire_tac st = res_atp_tac vampire_oracle ResAtp.Auto (!ResAtp.vampire_time) st;
45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 19128 diff changeset	21	fun eprover_tac st = res_atp_tac eprover_oracle ResAtp.Auto (!ResAtp.eprover_time) st;
18271 0e9a851db989 Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs. mengj parents: 18195 diff changeset	22
19193 45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 19128 diff changeset	23	fun vampireF_tac st = res_atp_tac vampire_oracle ResAtp.Fol (!ResAtp.vampire_time) st;
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	24
19193 45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 19128 diff changeset	25	fun vampireH_tac st = res_atp_tac vampire_oracle ResAtp.Hol (!ResAtp.vampire_time) st;
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	26
19193 45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 19128 diff changeset	27	fun eproverF_tac st = res_atp_tac eprover_oracle ResAtp.Fol (!ResAtp.eprover_time) st;
18271 0e9a851db989 Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs. mengj parents: 18195 diff changeset	28
19193 45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 19128 diff changeset	29	fun eproverH_tac st = res_atp_tac eprover_oracle ResAtp.Hol (!ResAtp.eprover_time) st;
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	30
18708 4b3dadb4fe33 setup: theory -> theory; wenzelm parents: 18271 diff changeset	31	val ResAtps_setup =
4b3dadb4fe33 setup: theory -> theory; wenzelm parents: 18271 diff changeset	32	Method.add_methods
19193 45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 19128 diff changeset	33	[("vampireF", ResAtp.atp_method vampireF_tac, "Vampire for FOL problems"),
45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 19128 diff changeset	34	("eproverF", ResAtp.atp_method eproverF_tac, "E prover for FOL problems"),
45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 19128 diff changeset	35	("vampireH", ResAtp.atp_method vampireH_tac, "Vampire for HOL problems"),
45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 19128 diff changeset	36	("eproverH", ResAtp.atp_method eproverH_tac, "E prover for HOL problems"),
45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 19128 diff changeset	37	("eprover", ResAtp.atp_method eprover_tac, "E prover for FOL and HOL problems"),
45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 19128 diff changeset	38	("vampire", ResAtp.atp_method vampire_tac, "Vampire for FOL and HOL problems")];
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	39
17907 c20e4bddcb11 * empty log message * mengj parents: 17905 diff changeset	40	end

author	wenzelm
	Sat, 20 May 2006 23:45:37 +0200
changeset 19695	7706aeac6cf1
parent 19193	45c8db82893d
child 19723	7602f74c914b
permissions	-rw-r--r--