src/HOL/SAT.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SAT.thy	Fri Sep 23 22:58:50 2005 +0200
@@ -0,0 +1,41 @@
+(*  Title:      HOL/SAT.thy
+    ID:         $Id$
+    Author:     Alwen Tiu, Tjark Weber
+    Copyright   2005
+
+Basic setup for the 'sat' tactic.
+*)
+
+header {* Reconstructing external resolution proofs for propositional logic *}
+
+theory SAT imports HOL
+
+uses "Tools/sat_solver.ML"
+     "Tools/cnf_funcs.ML"
+     "Tools/sat_funcs.ML"
+
+begin
+
+ML {* structure sat = SATFunc(structure cnf_struct = cnf); *}
+
+method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
+  "SAT solver"
+
+method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
+  "SAT solver (with definitional CNF)"
+
+(*
+method_setup cnf = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_tac) *}
+  "Transforming hypotheses in a goal into CNF"
+
+method_setup cnf_concl = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_concl_tac) *}
+  "Transforming the conclusion of a goal to CNF"
+
+method_setup cnf_thin = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_thin_tac) *}
+  "Same as cnf, but remove the original hypotheses"
+
+method_setup cnfx_thin = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnfx_thin_tac) *}
+  "Same as cnf_thin, but may introduce extra variables"
+*)
+
+end