isabelle: src/HOL/TPTP/ATP_Problem_Import.thy@89347c0cc6a3 (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
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	5	section \<open>ATP Problem Importer\<close>
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
72001 3e08311ada8e removed 'freeze_problem_consts' hack in TPTP tools, which wasn't compatible with post-2016 reforms to local theories blanchet parents: 69605 diff changeset	8	imports Complex_Main TPTP_Interpret "HOL-Library.Refute"
46324 e4bccf5ec61e added problem importer blanchet parents: diff changeset	9	begin
e4bccf5ec61e added problem importer blanchet parents: diff changeset	10
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	11	ML \<open>Proofterm.proofs := 0\<close>
47765 18f37b7aa6a6 more work on CASC setup blanchet parents: 47714 diff changeset	12
47670 24babc4b1925 added timeout argument to TPTP tools blanchet parents: 47557 diff changeset	13	declare [[show_consts]] (* for Refute *)
47765 18f37b7aa6a6 more work on CASC setup blanchet parents: 47714 diff changeset	14	declare [[smt_oracle]]
47670 24babc4b1925 added timeout argument to TPTP tools blanchet parents: 47557 diff changeset	15
47794 4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug) blanchet parents: 47790 diff changeset	16	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	17	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	18
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66453 diff changeset	19	ML_file \<open>atp_problem_import.ML\<close>
47794 4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug) blanchet parents: 47790 diff changeset	20
47785 d27bb852c430 more tweaking of TPTP/CASC setup blanchet parents: 47770 diff changeset	21	(*
57812 8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well blanchet parents: 52487 diff changeset	22	ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50 "$TPTP/Problems/PUZ/PUZ107^5.p" *}
64561 a7664ca9ffc5 updated CASC instructions + tuning blanchet parents: 63167 diff changeset	23	ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} 20 "$TPTP/Problems/SYO/SYO304^5.p" *}
47785 d27bb852c430 more tweaking of TPTP/CASC setup blanchet parents: 47770 diff changeset	24	*)
d27bb852c430 more tweaking of TPTP/CASC setup blanchet parents: 47770 diff changeset	25
46324 e4bccf5ec61e added problem importer blanchet parents: diff changeset	26	end

author	haftmann
	Thu, 19 Jun 2025 17:15:40 +0200
changeset 82734	89347c0cc6a3
parent 73684	a63d76ba0a03
permissions	-rw-r--r--