author | wenzelm |
Sat, 28 Jul 2012 20:36:25 +0200 | |
changeset 48589 | fb446a780d50 |
parent 47812 | bb477988edb4 |
child 48891 | c0eafbd55de3 |
permissions | -rw-r--r-- |
46324 | 1 |
(* Title: HOL/TPTP/ATP_Problem_Import.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* ATP Problem Importer *} |
|
47812 | 6 |
|
46324 | 7 |
theory ATP_Problem_Import |
47557
32f35b3d9e42
started integrating Nik's parser into TPTP command-line tools
blanchet
parents:
46324
diff
changeset
|
8 |
imports Complex_Main TPTP_Interpret |
47790 | 9 |
uses "sledgehammer_tactics.ML" |
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47790
diff
changeset
|
10 |
("atp_problem_import.ML") |
46324 | 11 |
begin |
12 |
||
47765 | 13 |
ML {* Proofterm.proofs := 0 *} |
14 |
||
47670 | 15 |
declare [[show_consts]] (* for Refute *) |
47765 | 16 |
declare [[smt_oracle]] |
47670 | 17 |
|
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47790
diff
changeset
|
18 |
declare [[unify_search_bound = 60]] |
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47790
diff
changeset
|
19 |
declare [[unify_trace_bound = 60]] |
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47790
diff
changeset
|
20 |
|
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47790
diff
changeset
|
21 |
use "atp_problem_import.ML" |
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47790
diff
changeset
|
22 |
|
47785 | 23 |
(* |
47794
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47790
diff
changeset
|
24 |
ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50 |
4ad62c5f9f88
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents:
47790
diff
changeset
|
25 |
"$TPTP/Problems/PUZ/PUZ107^5.p" *} |
47785 | 26 |
*) |
27 |
||
46324 | 28 |
end |