isabelle: src/HOL/SAT.thy@24b70433c2e8 (annotated)

17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	1	(* Title: HOL/SAT.thy
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	2	Author: Alwen Tiu, Tjark Weber
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	3	Copyright 2005
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	4
49989 34d0ac1bdac6 moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong blanchet parents: 49985 diff changeset	5	Basic setup for the 'sat' and 'satx' tactics.
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	6	*)
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	7
60758 d8d85a8172b5 isabelle update_cartouches; wenzelm parents: 58889 diff changeset	8	section \<open>Reconstructing external resolution proofs for propositional logic\<close>
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	9
26521 f8c4e79db153 tuned imports haftmann parents: 21588 diff changeset	10	theory SAT
63962 83a625d06e91 use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable boehmes parents: 60758 diff changeset	11	imports Argo
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	12	begin
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	13
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63962 diff changeset	14	ML_file \<open>Tools/prop_logic.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63962 diff changeset	15	ML_file \<open>Tools/sat_solver.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63962 diff changeset	16	ML_file \<open>Tools/sat.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63962 diff changeset	17	ML_file \<open>Tools/Argo/argo_sat_solver.ML\<close>
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46096 diff changeset	18
60758 d8d85a8172b5 isabelle update_cartouches; wenzelm parents: 58889 diff changeset	19	method_setup sat = \<open>Scan.succeed (SIMPLE_METHOD' o SAT.sat_tac)\<close>
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	20	"SAT solver"
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	21
60758 d8d85a8172b5 isabelle update_cartouches; wenzelm parents: 58889 diff changeset	22	method_setup satx = \<open>Scan.succeed (SIMPLE_METHOD' o SAT.satx_tac)\<close>
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	23	"SAT solver (with definitional CNF)"
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	24
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	25	end

author	paulson <lp15@cam.ac.uk>
	Tue, 30 May 2023 12:33:06 +0100
changeset 78127	24b70433c2e8
parent 69605	a96320074298
permissions	-rw-r--r--