src/HOL/SAT.thy
changeset 17618 1330157e156a
child 17625 1539d18e3e9f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SAT.thy	Fri Sep 23 22:58:50 2005 +0200
     1.3 @@ -0,0 +1,41 @@
     1.4 +(*  Title:      HOL/SAT.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Alwen Tiu, Tjark Weber
     1.7 +    Copyright   2005
     1.8 +
     1.9 +Basic setup for the 'sat' tactic.
    1.10 +*)
    1.11 +
    1.12 +header {* Reconstructing external resolution proofs for propositional logic *}
    1.13 +
    1.14 +theory SAT imports HOL
    1.15 +
    1.16 +uses "Tools/sat_solver.ML"
    1.17 +     "Tools/cnf_funcs.ML"
    1.18 +     "Tools/sat_funcs.ML"
    1.19 +
    1.20 +begin
    1.21 +
    1.22 +ML {* structure sat = SATFunc(structure cnf_struct = cnf); *}
    1.23 +
    1.24 +method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
    1.25 +  "SAT solver"
    1.26 +
    1.27 +method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
    1.28 +  "SAT solver (with definitional CNF)"
    1.29 +
    1.30 +(*
    1.31 +method_setup cnf = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_tac) *}
    1.32 +  "Transforming hypotheses in a goal into CNF"
    1.33 +
    1.34 +method_setup cnf_concl = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_concl_tac) *}
    1.35 +  "Transforming the conclusion of a goal to CNF"
    1.36 +
    1.37 +method_setup cnf_thin = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_thin_tac) *}
    1.38 +  "Same as cnf, but remove the original hypotheses"
    1.39 +
    1.40 +method_setup cnfx_thin = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnfx_thin_tac) *}
    1.41 +  "Same as cnf_thin, but may introduce extra variables"
    1.42 +*)
    1.43 +
    1.44 +end