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
```