isabelle: src/HOL/TPTP/ATP_Problem_Import.thy@8a635bf2c86c (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 *}
47812 bb477988edb4 use Nitpick as an oracle for finite problems blanchet parents: 47794 diff changeset	6
46324 e4bccf5ec61e added problem importer blanchet parents: diff changeset	7	theory ATP_Problem_Import
49985 5b4b0e4e5205 moved Refute to "HOL/Library" to speed up building "Main" even more blanchet parents: 48891 diff changeset	8	imports
5b4b0e4e5205 moved Refute to "HOL/Library" to speed up building "Main" even more blanchet parents: 48891 diff changeset	9	Complex_Main
5b4b0e4e5205 moved Refute to "HOL/Library" to speed up building "Main" even more blanchet parents: 48891 diff changeset	10	TPTP_Interpret
5b4b0e4e5205 moved Refute to "HOL/Library" to speed up building "Main" even more blanchet parents: 48891 diff changeset	11	"~~/src/HOL/Library/Refute"
46324 e4bccf5ec61e added problem importer blanchet parents: diff changeset	12	begin
e4bccf5ec61e added problem importer blanchet parents: diff changeset	13
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47812 diff changeset	14	ML_file "sledgehammer_tactics.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47812 diff changeset	15
47765 18f37b7aa6a6 more work on CASC setup blanchet parents: 47714 diff changeset	16	ML {* Proofterm.proofs := 0 *}
18f37b7aa6a6 more work on CASC setup blanchet parents: 47714 diff changeset	17
47670 24babc4b1925 added timeout argument to TPTP tools blanchet parents: 47557 diff changeset	18	declare [[show_consts]] (* for Refute *)
47765 18f37b7aa6a6 more work on CASC setup blanchet parents: 47714 diff changeset	19	declare [[smt_oracle]]
47670 24babc4b1925 added timeout argument to TPTP tools blanchet parents: 47557 diff changeset	20
47794 4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug) blanchet parents: 47790 diff changeset	21	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	22	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	23
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47812 diff changeset	24	ML_file "atp_problem_import.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	25
47785 d27bb852c430 more tweaking of TPTP/CASC setup blanchet parents: 47770 diff changeset	26	(*
47794 4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug) blanchet parents: 47790 diff changeset	27	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	28	"$TPTP/Problems/PUZ/PUZ107^5.p" *}
47785 d27bb852c430 more tweaking of TPTP/CASC setup blanchet parents: 47770 diff changeset	29	*)
d27bb852c430 more tweaking of TPTP/CASC setup blanchet parents: 47770 diff changeset	30
46324 e4bccf5ec61e added problem importer blanchet parents: diff changeset	31	end

author	Andreas Lochbihler
	Wed, 27 Feb 2013 13:48:15 +0100
changeset 51292	8a635bf2c86c
parent 49985	5b4b0e4e5205
child 52470	dedd7952a62c
permissions	-rw-r--r--