author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46435  e9c90516bc0d 
child 48129  933d43c31689 
permissions  rwrr 
46321  1 
(* Title: HOL/TPTP/ATP_Theory_Export.thy 
2 
Author: Jasmin Blanchette, TU Muenchen 

3 
*) 

4 

5 
header {* ATP Theory Exporter *} 

6 

7 
theory ATP_Theory_Export 

42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

8 
imports Complex_Main 
46321  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 {* 
45305  13 
open ATP_Problem; 
46321  14 
open ATP_Theory_Export; 
45305  15 
*} 
16 

17 
ML {* 

43468
c768f7adb711
fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies
blanchet
parents:
43400
diff
changeset

18 
val do_it = false; (* switch to "true" to generate the files *) 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset

19 
val thy = @{theory Complex_Main}; 
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 
46435  25 
"/tmp/axs_mono_native.dfg" 
45305  26 
> generate_tptp_inference_file_for_theory ctxt thy (DFG DFG_Sorted) 
46435  27 
"mono_native" 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset

28 
else 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset

29 
() 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

30 
*} 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

31 

a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

32 
ML {* 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset

33 
if do_it then 
45305  34 
"/tmp/infs_poly_guards.tptp" 
35 
> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_guards" 

43400
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset

36 
else 
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset

37 
() 
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 
ML {* 
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset

41 
if do_it then 
45305  42 
"/tmp/infs_poly_tags.tptp" 
43 
> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags" 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset

44 
else 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset

45 
() 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

46 
*} 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

47 

a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

48 
ML {* 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset

49 
if do_it then 
45305  50 
"/tmp/infs_poly_tags_uniform.tptp" 
51 
> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags_uniform" 

52 
else 

53 
() 

54 
*} 

55 

56 
ML {* 

57 
if do_it then 

58 
"/tmp/graph.out" > generate_tptp_graph_file_for_theory ctxt thy 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset

59 
else 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset

60 
() 
42607
c8673078f915
fix ROOT.ML and handle "readable_names" reference slightly more cleanly
blanchet
parents:
42602
diff
changeset

61 
*} 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

62 

a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

63 
end 