author | webertj |
Sun, 25 Sep 2005 01:12:49 +0200 | |
changeset 17631 | 152ab92e1009 |
parent 17627 | ff1923b1978b |
child 17722 | 8e098e040c2e |
permissions | -rw-r--r-- |
17618 | 1 |
(* Title: HOL/SAT.thy |
2 |
ID: $Id$ |
|
3 |
Author: Alwen Tiu, Tjark Weber |
|
4 |
Copyright 2005 |
|
5 |
||
17627 | 6 |
Basic setup for the 'sat' and 'satx' tactic. |
17618 | 7 |
*) |
8 |
||
9 |
header {* Reconstructing external resolution proofs for propositional logic *} |
|
10 |
||
11 |
theory SAT imports HOL |
|
12 |
||
17631
152ab92e1009
sat_solver.ML not loaded anymore (already loaded by Refute.thy)
webertj
parents:
17627
diff
changeset
|
13 |
uses (* "Tools/sat_solver.ML" -- already loaded by Refute.thy *) |
17618 | 14 |
"Tools/cnf_funcs.ML" |
15 |
"Tools/sat_funcs.ML" |
|
16 |
||
17 |
begin |
|
18 |
||
17627 | 19 |
ML {* structure sat = SATFunc(structure cnf = cnf); *} |
17618 | 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 |
||
17627 | 27 |
(* |
17618 | 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 |