author | blanchet |
Sun, 17 Jul 2011 14:12:45 +0200 | |
changeset 43863 | a43d61270142 |
parent 43862 | a14fdb8c0497 |
child 43996 | 4d1270ddf042 |
permissions | -rw-r--r-- |
43223
c9e87dc92d9e
renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
blanchet
parents:
43222
diff
changeset
|
1 |
(* Title: HOL/ex/atp_export.ML |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
3 |
Copyright 2011 |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
4 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
5 |
Export Isabelle theories as first-order TPTP inferences, exploiting |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
6 |
Sledgehammer's translation. |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
7 |
*) |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
8 |
|
43223
c9e87dc92d9e
renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
blanchet
parents:
43222
diff
changeset
|
9 |
signature ATP_EXPORT = |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
10 |
sig |
43494
13eefebbc4cb
make sure that enough type information is generated -- because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity
blanchet
parents:
43479
diff
changeset
|
11 |
val theorems_mentioned_in_proof_term : |
13eefebbc4cb
make sure that enough type information is generated -- because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity
blanchet
parents:
43479
diff
changeset
|
12 |
string list option -> thm -> string list |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
13 |
val generate_tptp_graph_file_for_theory : |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
14 |
Proof.context -> theory -> string -> unit |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
15 |
val generate_tptp_inference_file_for_theory : |
43400
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43351
diff
changeset
|
16 |
Proof.context -> theory -> string -> string -> unit |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
17 |
end; |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
18 |
|
43223
c9e87dc92d9e
renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
blanchet
parents:
43222
diff
changeset
|
19 |
structure ATP_Export : ATP_EXPORT = |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
20 |
struct |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
21 |
|
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
22 |
open ATP_Problem |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
23 |
open ATP_Translate |
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
24 |
open ATP_Proof |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
25 |
open ATP_Systems |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
26 |
|
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
27 |
val fact_name_of = prefix fact_prefix o ascii_of |
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 |
fun facts_of thy = |
43276 | 30 |
Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty |
43351
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43305
diff
changeset
|
31 |
true [] [] |
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43572
diff
changeset
|
32 |
|> filter (curry (op =) @{typ bool} o fastype_of |
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43572
diff
changeset
|
33 |
o Object_Logic.atomize_term thy o prop_of o snd) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
34 |
|
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
|
35 |
(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few |
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
|
36 |
fixes that seem to be missing over there; or maybe the two code portions are |
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
|
37 |
not doing the same? *) |
43498
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset
|
38 |
fun fold_body_thms thm_name all_names f = |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
39 |
let |
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
|
40 |
fun app n (PBody {thms, ...}) = |
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
41 |
thms |> fold (fn (_, (name, prop, body)) => fn x => |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
42 |
let |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
43 |
val body' = Future.join body |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
44 |
val n' = |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
45 |
n + (if name = "" orelse |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
46 |
(is_some all_names andalso |
43498
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset
|
47 |
not (member (op =) (the all_names) name)) orelse |
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset
|
48 |
(* uncommon case where the proved theorem occurs twice |
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset
|
49 |
(e.g., "Transitive_Closure.trancl_into_trancl") *) |
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset
|
50 |
n = 1 andalso name = thm_name then |
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
51 |
0 |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
52 |
else |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
53 |
1) |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
54 |
val x' = x |> n' <= 1 ? app n' body' |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
55 |
in (x' |> n = 1 ? f (name, prop, body')) end) |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
56 |
in fold (app 0) end |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
57 |
|
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
58 |
fun theorems_mentioned_in_proof_term all_names thm = |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
59 |
let |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
60 |
fun collect (s, _, _) = if s <> "" then insert (op =) s else I |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
61 |
val names = |
43498
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset
|
62 |
[] |> fold_body_thms (Thm.get_name_hint thm) all_names collect |
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset
|
63 |
[Thm.proof_body_of thm] |
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
64 |
|> map fact_name_of |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
65 |
in names end |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
66 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
67 |
fun interesting_const_names ctxt = |
43276 | 68 |
let val thy = Proof_Context.theory_of ctxt in |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
69 |
Sledgehammer_Filter.const_names_in_fact thy |
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
70 |
(Sledgehammer_Provers.is_built_in_const_for_prover ctxt eN) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
71 |
end |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
72 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
73 |
fun generate_tptp_graph_file_for_theory ctxt thy file_name = |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
74 |
let |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
75 |
val path = file_name |> Path.explode |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
76 |
val _ = File.write path "" |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
77 |
val axioms = Theory.all_axioms_of thy |> map fst |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
78 |
fun do_thm thm = |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
79 |
let |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
80 |
val name = Thm.get_name_hint thm |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
81 |
val s = |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
82 |
"[" ^ Thm.legacy_get_kind thm ^ "] " ^ |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
83 |
(if member (op =) axioms name then "A" else "T") ^ " " ^ |
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
84 |
prefix fact_prefix (ascii_of name) ^ ": " ^ |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
85 |
commas (theorems_mentioned_in_proof_term NONE thm) ^ "; " ^ |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
86 |
commas (map (prefix const_prefix o ascii_of) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
87 |
(interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n" |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
88 |
in File.append path s end |
43245 | 89 |
val thms = facts_of thy |> map snd |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
90 |
val _ = map do_thm thms |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
91 |
in () end |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
92 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
93 |
fun inference_term [] = NONE |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
94 |
| inference_term ss = |
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
95 |
ATerm ("inference", |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
96 |
[ATerm ("isabelle", []), |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
97 |
ATerm (tptp_empty_list, []), |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
98 |
ATerm (tptp_empty_list, map (fn s => ATerm (s, [])) ss)]) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
99 |
|> SOME |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
100 |
fun inference infers ident = |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
101 |
these (AList.lookup (op =) infers ident) |> inference_term |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
102 |
fun add_inferences_to_problem_line infers |
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
103 |
(Formula (ident, Axiom, phi, NONE, NONE)) = |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
104 |
Formula (ident, Lemma, phi, inference infers ident, NONE) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
105 |
| add_inferences_to_problem_line _ line = line |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
106 |
val add_inferences_to_problem = |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
107 |
map o apsnd o map o add_inferences_to_problem_line |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
108 |
|
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
109 |
fun ident_of_problem_line (Decl (ident, _, _)) = ident |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
110 |
| ident_of_problem_line (Formula (ident, _, _, _, _)) = ident |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
111 |
|
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
112 |
fun run_some_atp ctxt problem = |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
113 |
let |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
114 |
val thy = Proof_Context.theory_of ctxt |
43602 | 115 |
val prob_file = Path.explode "/tmp/prob.tptp" (* FIXME File.tmp_path (?) *) |
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
116 |
val {exec, arguments, proof_delims, known_failures, ...} = |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
117 |
get_atp thy spassN |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
118 |
val _ = problem |> tptp_lines_for_atp_problem FOF |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
119 |
|> File.write_list prob_file |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
120 |
val command = |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
121 |
File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^ |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
122 |
" " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^ |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
123 |
File.shell_path prob_file |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
124 |
in |
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43828
diff
changeset
|
125 |
TimeLimit.timeLimit (seconds 0.3) Isabelle_System.bash_output command |
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
126 |
|> fst |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
127 |
|> extract_tstplike_proof_and_outcome false true proof_delims |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
128 |
known_failures |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
129 |
|> snd |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
130 |
end |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
131 |
handle TimeLimit.TimeOut => SOME TimedOut |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
132 |
|
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
133 |
val likely_tautology_prefixes = |
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43566
diff
changeset
|
134 |
[@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}] |
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
135 |
|> map (fact_name_of o Context.theory_name) |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
136 |
|
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
137 |
fun is_problem_line_tautology ctxt (Formula (ident, _, phi, _, _)) = |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
138 |
exists (fn prefix => String.isPrefix prefix ident) |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
139 |
likely_tautology_prefixes andalso |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
140 |
is_none (run_some_atp ctxt |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
141 |
[(factsN, [Formula (ident, Conjecture, phi, NONE, NONE)])]) |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
142 |
| is_problem_line_tautology _ _ = false |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
143 |
|
43499 | 144 |
structure String_Graph = Graph(type key = string val ord = string_ord); |
145 |
||
146 |
fun order_facts ord = sort (ord o pairself ident_of_problem_line) |
|
147 |
fun order_problem_facts _ [] = [] |
|
148 |
| order_problem_facts ord ((heading, lines) :: problem) = |
|
149 |
if heading = factsN then (heading, order_facts ord lines) :: problem |
|
150 |
else (heading, lines) :: order_problem_facts ord problem |
|
151 |
||
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43602
diff
changeset
|
152 |
fun generate_tptp_inference_file_for_theory ctxt thy type_enc file_name = |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
153 |
let |
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
154 |
val format = FOF |
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43602
diff
changeset
|
155 |
val type_enc = type_enc |> type_enc_from_string |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
156 |
val path = file_name |> Path.explode |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
157 |
val _ = File.write path "" |
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43572
diff
changeset
|
158 |
val facts = facts_of thy |
42881
dbdfe2d5b6ab
automatically use "metisFT" when typed helpers are necessary
blanchet
parents:
42837
diff
changeset
|
159 |
val (atp_problem, _, _, _, _, _, _) = |
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43572
diff
changeset
|
160 |
facts |
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43572
diff
changeset
|
161 |
|> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th)) |
43828
e07a2c4cbad8
move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)
blanchet
parents:
43804
diff
changeset
|
162 |
|> prepare_atp_problem ctxt format Axiom Axiom type_enc true true |
43863
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents:
43862
diff
changeset
|
163 |
(rpair [] o map (introduce_combinators ctxt)) |
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents:
43862
diff
changeset
|
164 |
false true [] @{prop False} |
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
165 |
val atp_problem = |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
166 |
atp_problem |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
167 |
|> map (apsnd (filter_out (is_problem_line_tautology ctxt))) |
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43572
diff
changeset
|
168 |
val all_names = facts |> map (Thm.get_name_hint o snd) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
169 |
val infers = |
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43572
diff
changeset
|
170 |
facts |> map (fn (_, th) => |
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43572
diff
changeset
|
171 |
(fact_name_of (Thm.get_name_hint th), |
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43572
diff
changeset
|
172 |
theorems_mentioned_in_proof_term (SOME all_names) th)) |
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
173 |
val all_atp_problem_names = |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
174 |
atp_problem |> maps (map ident_of_problem_line o snd) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
175 |
val infers = |
43499 | 176 |
infers |> filter (member (op =) all_atp_problem_names o fst) |
177 |
|> map (apsnd (filter (member (op =) all_atp_problem_names))) |
|
178 |
val ordered_names = |
|
179 |
String_Graph.empty |
|
180 |
|> fold (String_Graph.new_node o rpair ()) all_atp_problem_names |
|
181 |
|> fold (fn (to, froms) => |
|
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
182 |
fold (fn from => String_Graph.add_edge (from, to)) froms) |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
183 |
infers |
43499 | 184 |
|> String_Graph.topological_order |
185 |
val order_tab = |
|
186 |
Symtab.empty |
|
187 |
|> fold (Symtab.insert (op =)) |
|
188 |
(ordered_names ~~ (1 upto length ordered_names)) |
|
189 |
val name_ord = int_ord o pairself (the o Symtab.lookup order_tab) |
|
190 |
val atp_problem = |
|
191 |
atp_problem |> add_inferences_to_problem infers |
|
192 |
|> order_problem_facts name_ord |
|
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
193 |
val ss = tptp_lines_for_atp_problem FOF atp_problem |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
194 |
val _ = app (File.append path) ss |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
195 |
in () end |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
196 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
197 |
end; |