isabelle: src/HOL/Tools/res_atp_methods.ML@ad95084a5c63 (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 *)
19723 7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	11	fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms n thm =
23590 ad95084a5c63 renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac; wenzelm parents: 19723 diff changeset	12	(EVERY' [rtac ccontr, ObjectLogic.atomize_prems_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)
19723 7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	16	(ResAtp.write_subgoal_file dfg mode ctxt negs user_thms n, timeLimit))))] n thm) handle (Fail _) => Seq.empty;
7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	17
7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	18	(* vampire, eprover and spass 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
19723 7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	20	fun vampire_tac st = res_atp_tac false vampire_oracle ResAtp.Auto (!ResAtp.vampire_time) st;
7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	21	fun eprover_tac st = res_atp_tac false eprover_oracle ResAtp.Auto (!ResAtp.eprover_time) st;
7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	22	fun spass_tac st = res_atp_tac true spass_oracle ResAtp.Auto (!ResAtp.spass_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	23
18271 0e9a851db989 Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs. mengj parents: 18195 diff changeset	24
19723 7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	25	fun vampireF_tac st = res_atp_tac false 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	26
19723 7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	27	fun vampireH_tac st = res_atp_tac false vampire_oracle ResAtp.Hol (!ResAtp.vampire_time) st;
7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	28
7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	29	fun eproverF_tac st = res_atp_tac false eprover_oracle ResAtp.Fol (!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
19723 7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	31	fun eproverH_tac st = res_atp_tac false eprover_oracle ResAtp.Hol (!ResAtp.eprover_time) st;
18271 0e9a851db989 Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs. mengj parents: 18195 diff changeset	32
19723 7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	33	fun spassF_tac st = res_atp_tac true spass_oracle ResAtp.Fol (!ResAtp.spass_time) st;
7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	34
7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	35	fun spassH_tac st = res_atp_tac true spass_oracle ResAtp.Hol (!ResAtp.spass_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	36
18708 4b3dadb4fe33 setup: theory -> theory; wenzelm parents: 18271 diff changeset	37	val ResAtps_setup =
4b3dadb4fe33 setup: theory -> theory; wenzelm parents: 18271 diff changeset	38	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	39	[("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	40	("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	41	("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	42	("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	43	("eprover", ResAtp.atp_method eprover_tac, "E prover for FOL and HOL problems"),
19723 7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	44	("vampire", ResAtp.atp_method vampire_tac, "Vampire for FOL and HOL problems"),
7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	45	("spassF", ResAtp.atp_method spassF_tac, "SPASS for FOL problems"),
7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	46	("spassH", ResAtp.atp_method spassH_tac, "SPASS for HOL problems"),
7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	47	("spass", ResAtp.atp_method spass_tac, "SPASS 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	48
17907 c20e4bddcb11 * empty log message * mengj parents: 17905 diff changeset	49	end

author	wenzelm
	Thu, 05 Jul 2007 20:01:26 +0200
changeset 23590	ad95084a5c63
parent 19723	7602f74c914b
child 24215	5458fbf18276
permissions	-rw-r--r--