author | blanchet |
Tue, 26 Jun 2012 11:14:39 +0200 | |
changeset 48129 | 933d43c31689 |
parent 46435 | e9c90516bc0d |
child 48141 | 1b864c4a3306 |
permissions | -rw-r--r-- |
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" |
48129
933d43c31689
removed support for unsorted DFG, now that SPASS 3.7 is no longer supported
blanchet
parents:
46435
diff
changeset
|
26 |
|> generate_tptp_inference_file_for_theory ctxt thy DFG "mono_native" |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
27 |
else |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
28 |
() |
42602
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 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
31 |
ML {* |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
32 |
if do_it then |
45305 | 33 |
"/tmp/infs_poly_guards.tptp" |
34 |
|> 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
|
35 |
else |
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
36 |
() |
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 |
ML {* |
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
40 |
if do_it then |
45305 | 41 |
"/tmp/infs_poly_tags.tptp" |
42 |
|> 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
|
43 |
else |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
44 |
() |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
45 |
*} |
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 |
ML {* |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
48 |
if do_it then |
45305 | 49 |
"/tmp/infs_poly_tags_uniform.tptp" |
50 |
|> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags_uniform" |
|
51 |
else |
|
52 |
() |
|
53 |
*} |
|
54 |
||
55 |
ML {* |
|
56 |
if do_it then |
|
57 |
"/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
|
58 |
else |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
59 |
() |
42607
c8673078f915
fix ROOT.ML and handle "readable_names" reference slightly more cleanly
blanchet
parents:
42602
diff
changeset
|
60 |
*} |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
61 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
62 |
end |