author | wenzelm |
Sat, 14 Jan 2012 12:36:43 +0100 | |
changeset 46204 | df1369a42393 |
parent 45305 | 3e09961326ce |
permissions | -rw-r--r-- |
43223
c9e87dc92d9e
renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
blanchet
parents:
43110
diff
changeset
|
1 |
theory ATP_Export |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
2 |
imports Complex_Main |
43223
c9e87dc92d9e
renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
blanchet
parents:
43110
diff
changeset
|
3 |
uses "atp_export.ML" |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
4 |
begin |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
5 |
|
42607
c8673078f915
fix ROOT.ML and handle "readable_names" reference slightly more cleanly
blanchet
parents:
42602
diff
changeset
|
6 |
ML {* |
45305 | 7 |
open ATP_Problem; |
8 |
open ATP_Export; |
|
9 |
*} |
|
10 |
||
11 |
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
|
12 |
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
|
13 |
val thy = @{theory Complex_Main}; |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
14 |
val ctxt = @{context} |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
15 |
*} |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
16 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
17 |
ML {* |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
18 |
if do_it then |
45305 | 19 |
"/tmp/axs_mono_simple.dfg" |
20 |
|> generate_tptp_inference_file_for_theory ctxt thy (DFG DFG_Sorted) |
|
21 |
"mono_simple" |
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
22 |
else |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
23 |
() |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
24 |
*} |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
25 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
26 |
ML {* |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
27 |
if do_it then |
45305 | 28 |
"/tmp/infs_poly_guards.tptp" |
29 |
|> 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
|
30 |
else |
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
31 |
() |
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
32 |
*} |
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
33 |
|
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
34 |
ML {* |
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
35 |
if do_it then |
45305 | 36 |
"/tmp/infs_poly_tags.tptp" |
37 |
|> 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
|
38 |
else |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
39 |
() |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
40 |
*} |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
41 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
42 |
ML {* |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
43 |
if do_it then |
45305 | 44 |
"/tmp/infs_poly_tags_uniform.tptp" |
45 |
|> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags_uniform" |
|
46 |
else |
|
47 |
() |
|
48 |
*} |
|
49 |
||
50 |
ML {* |
|
51 |
if do_it then |
|
52 |
"/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
|
53 |
else |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
54 |
() |
42607
c8673078f915
fix ROOT.ML and handle "readable_names" reference slightly more cleanly
blanchet
parents:
42602
diff
changeset
|
55 |
*} |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
56 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
57 |
end |