| author | huffman |
| Wed, 17 Aug 2011 15:12:34 -0700 | |
| changeset 44262 | 355d5438f5fb |
| parent 43804 | eb9be23db2b7 |
| child 44402 | f0bc74b9161e |
| 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 {*
|
|
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
|
7 |
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
|
8 |
val thy = @{theory Complex_Main};
|
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
9 |
val ctxt = @{context}
|
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
10 |
*} |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
11 |
|
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
12 |
ML {*
|
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
13 |
if do_it then |
|
43400
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
14 |
ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_preds" |
|
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
15 |
"/tmp/infs_poly_preds.tptp" |
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
16 |
else |
|
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
17 |
() |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
18 |
*} |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
19 |
|
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
20 |
ML {*
|
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
21 |
if do_it then |
|
43400
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
22 |
ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags" |
|
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
23 |
"/tmp/infs_poly_tags.tptp" |
|
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
24 |
else |
|
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
25 |
() |
|
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
26 |
*} |
|
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
27 |
|
|
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
28 |
ML {*
|
|
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
29 |
if do_it then |
|
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
30 |
ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags_heavy" |
|
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
31 |
"/tmp/infs_poly_tags_heavy.tptp" |
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
32 |
else |
|
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
33 |
() |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
34 |
*} |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
35 |
|
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
36 |
ML {*
|
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
37 |
if do_it then |
|
43223
c9e87dc92d9e
renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
blanchet
parents:
43110
diff
changeset
|
38 |
ATP_Export.generate_tptp_graph_file_for_theory ctxt thy |
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
39 |
"/tmp/graph.out" |
|
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
40 |
else |
|
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
41 |
() |
|
42607
c8673078f915
fix ROOT.ML and handle "readable_names" reference slightly more cleanly
blanchet
parents:
42602
diff
changeset
|
42 |
*} |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
43 |
|
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
44 |
end |