isabelle: src/HOL/TPTP/ATP_Problem_Import.thy@4ad62c5f9f88 (annotated)

46324 e4bccf5ec61e added problem importer blanchet parents: diff changeset	1	(* Title: HOL/TPTP/ATP_Problem_Import.thy
e4bccf5ec61e added problem importer blanchet parents: diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
e4bccf5ec61e added problem importer blanchet parents: diff changeset	3	*)
e4bccf5ec61e added problem importer blanchet parents: diff changeset	4
e4bccf5ec61e added problem importer blanchet parents: diff changeset	5	header {* ATP Problem Importer *}
e4bccf5ec61e added problem importer blanchet parents: diff changeset	6	theory ATP_Problem_Import
47557 32f35b3d9e42 started integrating Nik's parser into TPTP command-line tools blanchet parents: 46324 diff changeset	7	imports Complex_Main TPTP_Interpret
47790 2e1636e45770 move file to where it belongs blanchet parents: 47788 diff changeset	8	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	9	("atp_problem_import.ML")
46324 e4bccf5ec61e added problem importer blanchet parents: diff changeset	10	begin
e4bccf5ec61e added problem importer blanchet parents: diff changeset	11
47765 18f37b7aa6a6 more work on CASC setup blanchet parents: 47714 diff changeset	12	ML {* Proofterm.proofs := 0 *}
18f37b7aa6a6 more work on CASC setup blanchet parents: 47714 diff changeset	13
47670 24babc4b1925 added timeout argument to TPTP tools blanchet parents: 47557 diff changeset	14	declare [[show_consts]] (* for Refute *)
47765 18f37b7aa6a6 more work on CASC setup blanchet parents: 47714 diff changeset	15	declare [[smt_oracle]]
47670 24babc4b1925 added timeout argument to TPTP tools blanchet parents: 47557 diff changeset	16
47794 4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug) blanchet parents: 47790 diff changeset	17	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	18	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	19
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug) blanchet parents: 47790 diff changeset	20	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	21
47785 d27bb852c430 more tweaking of TPTP/CASC setup blanchet parents: 47770 diff changeset	22	(*
47794 4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug) blanchet parents: 47790 diff changeset	23	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	24	"$TPTP/Problems/PUZ/PUZ107^5.p" *}
47785 d27bb852c430 more tweaking of TPTP/CASC setup blanchet parents: 47770 diff changeset	25	*)
d27bb852c430 more tweaking of TPTP/CASC setup blanchet parents: 47770 diff changeset	26
46324 e4bccf5ec61e added problem importer blanchet parents: diff changeset	27	end

author	blanchet
	Fri, 27 Apr 2012 15:24:37 +0200
changeset 47794	4ad62c5f9f88
parent 47790	2e1636e45770
child 47812	bb477988edb4
permissions	-rw-r--r--