| author | wenzelm |
| Fri Mar 07 22:30:58 2014 +0100 (2014-03-07) | |
| changeset 55990 | 41c6b99c5fb7 |
| parent 55239 | 97921d23ebe3 |
| child 58889 | 5b7a9633cfa8 |
| permissions | -rw-r--r-- |
1 (* Title: HOL/SAT.thy
2 Author: Alwen Tiu, Tjark Weber
3 Copyright 2005
5 Basic setup for the 'sat' and 'satx' tactics.
6 *)
8 header {* Reconstructing external resolution proofs for propositional logic *}
10 theory SAT
11 imports HOL
12 begin
14 ML_file "Tools/prop_logic.ML"
15 ML_file "Tools/sat_solver.ML"
16 ML_file "Tools/sat.ML"
18 method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o SAT.sat_tac) *}
19 "SAT solver"
21 method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o SAT.satx_tac) *}
22 "SAT solver (with definitional CNF)"
24 end