isabelle: src/HOL/TPTP/ATP_Theory_Export.thy@94a9650f79fb (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
46321 484dc68c8c89 renamed theory exporter blanchet parents: 45305 diff changeset	9	uses "atp_theory_export.ML"
42602 a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning blanchet parents: diff changeset	10	begin
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning blanchet parents: diff changeset	11
42607 c8673078f915 fix ROOT.ML and handle "readable_names" reference slightly more cleanly blanchet parents: 42602 diff changeset	12	ML {*
48375 48628962976b tuning blanchet parents: 48302 diff changeset	13	open ATP_Problem
48628962976b tuning blanchet parents: 48302 diff changeset	14	open ATP_Theory_Export
45305 3e09961326ce also export DFG formats blanchet parents: 44402 diff changeset	15	*}
3e09961326ce also export DFG formats blanchet parents: 44402 diff changeset	16
3e09961326ce also export DFG formats blanchet parents: 44402 diff changeset	17	ML {*
48375 48628962976b tuning blanchet parents: 48302 diff changeset	18	val do_it = false (* switch to "true" to generate the files *)
48628962976b tuning blanchet parents: 48302 diff changeset	19	val thy = @{theory List}
42602 a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning blanchet parents: diff changeset	20	val ctxt = @{context}
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning blanchet parents: diff changeset	21	*}
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	ML {*
42646 4781fcd53572 replaced some Unsynchronized.refs with Config.Ts blanchet parents: 42607 diff changeset	24	if do_it then
48301 e5c5037a3104 started implementing MaSh client-side I/O blanchet parents: 48239 diff changeset	25	"/tmp/axs_tc_native.dfg"
e5c5037a3104 started implementing MaSh client-side I/O blanchet parents: 48239 diff changeset	26	\|> generate_atp_inference_file_for_theory ctxt thy (DFG Polymorphic)
e5c5037a3104 started implementing MaSh client-side I/O blanchet parents: 48239 diff changeset	27	"tc_native"
e5c5037a3104 started implementing MaSh client-side I/O blanchet parents: 48239 diff changeset	28	else
e5c5037a3104 started implementing MaSh client-side I/O blanchet parents: 48239 diff changeset	29	()
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	ML {*
e5c5037a3104 started implementing MaSh client-side I/O blanchet parents: 48239 diff changeset	33	if do_it then
48213 d20add034f64 first go at generating files for MaSh (machine-learning Sledgehammer) blanchet parents: 48145 diff changeset	34	"/tmp/infs_poly_guards_query_query.tptp"
48234 06216c789ac9 moved MaSh into own files blanchet parents: 48228 diff changeset	35	\|> generate_atp_inference_file_for_theory ctxt thy FOF
48217 8994afe09c18 more precise dependencies -- eliminate tautologies blanchet parents: 48216 diff changeset	36	"poly_guards_query_query"
43400 3d03f4472883 use more appropriate type systems for ATP exporter blanchet parents: 43223 diff changeset	37	else
3d03f4472883 use more appropriate type systems for ATP exporter blanchet parents: 43223 diff changeset	38	()
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	ML {*
3d03f4472883 use more appropriate type systems for ATP exporter blanchet parents: 43223 diff changeset	42	if do_it then
48145 f7b31782e632 compile blanchet parents: 48141 diff changeset	43	"/tmp/infs_poly_tags_query_query.tptp"
48234 06216c789ac9 moved MaSh into own files blanchet parents: 48228 diff changeset	44	\|> generate_atp_inference_file_for_theory ctxt thy FOF
48217 8994afe09c18 more precise dependencies -- eliminate tautologies blanchet parents: 48216 diff changeset	45	"poly_tags_query_query"
45305 3e09961326ce also export DFG formats blanchet parents: 44402 diff changeset	46	else
3e09961326ce also export DFG formats blanchet parents: 44402 diff changeset	47	()
3e09961326ce also export DFG formats blanchet parents: 44402 diff changeset	48	*}
3e09961326ce also export DFG formats blanchet parents: 44402 diff changeset	49
42602 a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning blanchet parents: diff changeset	50	end

author	wenzelm
	Tue, 24 Jul 2012 21:36:53 +0200
changeset 48487	94a9650f79fb
parent 48375	48628962976b
child 48891	c0eafbd55de3
permissions	-rw-r--r--