isabelle: src/HOL/TPTP/ATP_Theory_Export.thy@a600c017f814 (annotated)

46321 484dc68c8c89 renamed theory exporter blanchet parents: 45305 diff changeset	1	(* Title: HOL/TPTP/ATP_Theory_Export.thy
484dc68c8c89 renamed theory exporter blanchet parents: 45305 diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
484dc68c8c89 renamed theory exporter blanchet parents: 45305 diff changeset	3	*)
484dc68c8c89 renamed theory exporter blanchet parents: 45305 diff changeset	4
484dc68c8c89 renamed theory exporter blanchet parents: 45305 diff changeset	5	header {* ATP Theory Exporter *}
484dc68c8c89 renamed theory exporter blanchet parents: 45305 diff changeset	6
484dc68c8c89 renamed theory exporter blanchet parents: 45305 diff changeset	7	theory ATP_Theory_Export
48302 6cf5e58f1185 more implementation work on MaSh blanchet parents: 48301 diff changeset	8	imports Complex_Main
42602 a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning blanchet parents: diff changeset	9	begin
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning blanchet parents: diff changeset	10
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48375 diff changeset	11	ML_file "atp_theory_export.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48375 diff changeset	12
42607 c8673078f915 fix ROOT.ML and handle "readable_names" reference slightly more cleanly blanchet parents: 42602 diff changeset	13	ML {*
48375 48628962976b tuning blanchet parents: 48302 diff changeset	14	open ATP_Problem
48628962976b tuning blanchet parents: 48302 diff changeset	15	open ATP_Theory_Export
45305 3e09961326ce also export DFG formats blanchet parents: 44402 diff changeset	16	*}
3e09961326ce also export DFG formats blanchet parents: 44402 diff changeset	17
3e09961326ce also export DFG formats blanchet parents: 44402 diff changeset	18	ML {*
48375 48628962976b tuning blanchet parents: 48302 diff changeset	19	val do_it = false (* switch to "true" to generate the files *)
48628962976b tuning blanchet parents: 48302 diff changeset	20	val thy = @{theory List}
42602 a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning blanchet parents: diff changeset	21	val ctxt = @{context}
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning blanchet parents: diff changeset	22	*}
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning blanchet parents: diff changeset	23
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning blanchet parents: diff changeset	24	ML {*
42646 4781fcd53572 replaced some Unsynchronized.refs with Config.Ts blanchet parents: 42607 diff changeset	25	if do_it then
48301 e5c5037a3104 started implementing MaSh client-side I/O blanchet parents: 48239 diff changeset	26	"/tmp/axs_tc_native.dfg"
e5c5037a3104 started implementing MaSh client-side I/O blanchet parents: 48239 diff changeset	27	\|> generate_atp_inference_file_for_theory ctxt thy (DFG Polymorphic)
e5c5037a3104 started implementing MaSh client-side I/O blanchet parents: 48239 diff changeset	28	"tc_native"
e5c5037a3104 started implementing MaSh client-side I/O blanchet parents: 48239 diff changeset	29	else
e5c5037a3104 started implementing MaSh client-side I/O blanchet parents: 48239 diff changeset	30	()
e5c5037a3104 started implementing MaSh client-side I/O blanchet parents: 48239 diff changeset	31	*}
e5c5037a3104 started implementing MaSh client-side I/O blanchet parents: 48239 diff changeset	32
e5c5037a3104 started implementing MaSh client-side I/O blanchet parents: 48239 diff changeset	33	ML {*
e5c5037a3104 started implementing MaSh client-side I/O blanchet parents: 48239 diff changeset	34	if do_it then
48213 d20add034f64 first go at generating files for MaSh (machine-learning Sledgehammer) blanchet parents: 48145 diff changeset	35	"/tmp/infs_poly_guards_query_query.tptp"
48234 06216c789ac9 moved MaSh into own files blanchet parents: 48228 diff changeset	36	\|> generate_atp_inference_file_for_theory ctxt thy FOF
48217 8994afe09c18 more precise dependencies -- eliminate tautologies blanchet parents: 48216 diff changeset	37	"poly_guards_query_query"
43400 3d03f4472883 use more appropriate type systems for ATP exporter blanchet parents: 43223 diff changeset	38	else
3d03f4472883 use more appropriate type systems for ATP exporter blanchet parents: 43223 diff changeset	39	()
3d03f4472883 use more appropriate type systems for ATP exporter blanchet parents: 43223 diff changeset	40	*}
3d03f4472883 use more appropriate type systems for ATP exporter blanchet parents: 43223 diff changeset	41
3d03f4472883 use more appropriate type systems for ATP exporter blanchet parents: 43223 diff changeset	42	ML {*
3d03f4472883 use more appropriate type systems for ATP exporter blanchet parents: 43223 diff changeset	43	if do_it then
48145 f7b31782e632 compile blanchet parents: 48141 diff changeset	44	"/tmp/infs_poly_tags_query_query.tptp"
48234 06216c789ac9 moved MaSh into own files blanchet parents: 48228 diff changeset	45	\|> generate_atp_inference_file_for_theory ctxt thy FOF
48217 8994afe09c18 more precise dependencies -- eliminate tautologies blanchet parents: 48216 diff changeset	46	"poly_tags_query_query"
45305 3e09961326ce also export DFG formats blanchet parents: 44402 diff changeset	47	else
3e09961326ce also export DFG formats blanchet parents: 44402 diff changeset	48	()
3e09961326ce also export DFG formats blanchet parents: 44402 diff changeset	49	*}
3e09961326ce also export DFG formats blanchet parents: 44402 diff changeset	50
42602 a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning blanchet parents: diff changeset	51	end

author	wenzelm
	Tue, 11 Sep 2012 22:54:12 +0200
changeset 49294	a600c017f814
parent 48891	c0eafbd55de3
child 51645	86e8c87e1f1b
permissions	-rw-r--r--