| author | blanchet |
| Thu, 05 May 2011 02:27:02 +0200 | |
| changeset 42690 | 4d29b4785f43 |
| parent 42646 | 4781fcd53572 |
| child 43110 | 99bf2b38d3ef |
| permissions | -rw-r--r-- |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
1 |
theory TPTP_Export |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
2 |
imports Complex_Main |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
3 |
uses "tptp_export.ML" |
|
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 |
|
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
6 |
declare [[sledgehammer_atp_readable_names = false]] |
|
42607
c8673078f915
fix ROOT.ML and handle "readable_names" reference slightly more cleanly
blanchet
parents:
42602
diff
changeset
|
7 |
|
|
c8673078f915
fix ROOT.ML and handle "readable_names" reference slightly more cleanly
blanchet
parents:
42602
diff
changeset
|
8 |
ML {*
|
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
9 |
val do_it = false; (* switch to true to generate files *) |
|
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
10 |
val thy = @{theory Complex_Main};
|
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
11 |
val ctxt = @{context}
|
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
12 |
*} |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
13 |
|
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
14 |
ML {*
|
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
15 |
if do_it then |
|
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
16 |
TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy true |
|
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
17 |
"/tmp/infs_full_types.tptp" |
|
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
18 |
else |
|
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
19 |
() |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
20 |
*} |
|
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 |
ML {*
|
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
23 |
if do_it then |
|
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
24 |
TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy false |
|
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
25 |
"/tmp/infs_partial_types.tptp" |
|
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
26 |
else |
|
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
27 |
() |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
28 |
*} |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
29 |
|
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
30 |
ML {*
|
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
31 |
if do_it then |
|
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
32 |
TPTP_Export.generate_tptp_graph_file_for_theory ctxt thy |
|
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
33 |
"/tmp/graph.out" |
|
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
34 |
else |
|
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
35 |
() |
|
42607
c8673078f915
fix ROOT.ML and handle "readable_names" reference slightly more cleanly
blanchet
parents:
42602
diff
changeset
|
36 |
*} |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
37 |
|
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
38 |
end |