src/HOL/SAT.thy
author webertj
Sat Sep 24 13:54:35 2005 +0200 (2005-09-24)
changeset 17627 ff1923b1978b
parent 17625 1539d18e3e9f
child 17631 152ab92e1009
permissions -rw-r--r--
cnf_struct renamed to cnf
     1 (*  Title:      HOL/SAT.thy
     2     ID:         $Id$
     3     Author:     Alwen Tiu, Tjark Weber
     4     Copyright   2005
     5 
     6 Basic setup for the 'sat' and 'satx' tactic.
     7 *)
     8 
     9 header {* Reconstructing external resolution proofs for propositional logic *}
    10 
    11 theory SAT imports HOL
    12 
    13 uses "Tools/sat_solver.ML"
    14      "Tools/cnf_funcs.ML"
    15      "Tools/sat_funcs.ML"
    16 
    17 begin
    18 
    19 ML {* structure sat = SATFunc(structure cnf = cnf); *}
    20 
    21 method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
    22   "SAT solver"
    23 
    24 method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
    25   "SAT solver (with definitional CNF)"
    26 
    27 (*
    28 method_setup cnf = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_tac) *}
    29   "Transforming hypotheses in a goal into CNF"
    30 
    31 method_setup cnf_concl = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_concl_tac) *}
    32   "Transforming the conclusion of a goal to CNF"
    33 
    34 method_setup cnf_thin = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_thin_tac) *}
    35   "Same as cnf, but remove the original hypotheses"
    36 
    37 method_setup cnfx_thin = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnfx_thin_tac) *}
    38   "Same as cnf_thin, but may introduce extra variables"
    39 *)
    40 
    41 end