isabelle: src/HOL/SAT.thy@0a2371e7ced3 (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
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	8	header {* Reconstructing external resolution proofs for propositional logic *}
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
49989 34d0ac1bdac6 moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong blanchet parents: 49985 diff changeset	11	imports HOL
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
49989 34d0ac1bdac6 moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong blanchet parents: 49985 diff changeset	14	ML_file "Tools/prop_logic.ML"
34d0ac1bdac6 moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong blanchet parents: 49985 diff changeset	15	ML_file "Tools/sat_solver.ML"
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46096 diff changeset	16	ML_file "Tools/sat_funcs.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46096 diff changeset	17
32232 6c394343360f proper context for SAT tactics; wenzelm parents: 30549 diff changeset	18	ML {* structure sat = SATFunc(cnf) *}
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	19
32232 6c394343360f proper context for SAT tactics; wenzelm parents: 30549 diff changeset	20	method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *}
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	21	"SAT solver"
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	22
32232 6c394343360f proper context for SAT tactics; wenzelm parents: 30549 diff changeset	23	method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o sat.satx_tac) *}
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	24	"SAT solver (with definitional CNF)"
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	25
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	26	end

author	haftmann
	Fri, 15 Feb 2013 08:31:31 +0100
changeset 51143	0a2371e7ced3
parent 49989	34d0ac1bdac6
child 55239	97921d23ebe3
permissions	-rw-r--r--