isabelle: src/HOL/ResAtpMethods.thy@50aaae6ae4db (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
19721 515f660c0ccb Added in SPASS oracle. mengj parents: 19193 diff changeset	5	header {* ATP setup (Vampire, E prover and SPASS) *}
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	6
17958 c0bc47e944de proper header; wenzelm parents: 17939 diff changeset	7	theory ResAtpMethods
c0bc47e944de proper header; wenzelm parents: 17939 diff changeset	8	imports Reconstruction
c0bc47e944de proper header; wenzelm parents: 17939 diff changeset	9	uses
c0bc47e944de proper header; wenzelm parents: 17939 diff changeset	10	"Tools/res_atp_provers.ML"
c0bc47e944de proper header; wenzelm parents: 17939 diff changeset	11	("Tools/res_atp_methods.ML")
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	12
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	begin
17939 3925ab7b8a18 Merged theory ResAtpOracle.thy into ResAtpMethods.thy mengj parents: 17907 diff changeset	14
19193 45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 18201 diff changeset	15	oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 18201 diff changeset	16	oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}
19721 515f660c0ccb Added in SPASS oracle. mengj parents: 19193 diff changeset	17	oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *}
17939 3925ab7b8a18 Merged theory ResAtpOracle.thy into ResAtpMethods.thy mengj parents: 17907 diff changeset	18
17958 c0bc47e944de proper header; wenzelm parents: 17939 diff changeset	19	use "Tools/res_atp_methods.ML"
c0bc47e944de proper header; wenzelm parents: 17939 diff changeset	20	setup ResAtpMethods.ResAtps_setup
17939 3925ab7b8a18 Merged theory ResAtpOracle.thy into ResAtpMethods.thy mengj parents: 17907 diff changeset	21
17907 c20e4bddcb11 * empty log message * mengj parents: 17905 diff changeset	22	end

author	haftmann
	Tue, 08 Aug 2006 08:19:44 +0200
changeset 20355	50aaae6ae4db
parent 19721	515f660c0ccb
permissions	-rw-r--r--