src/HOL/SAT.thy
author wenzelm
Sat, 01 Feb 2014 21:09:53 +0100
changeset 55239 97921d23ebe3
parent 49989 34d0ac1bdac6
child 58889 5b7a9633cfa8
permissions -rw-r--r--
more standard file/module names;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     1
(*  Title:      HOL/SAT.thy
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     2
    Author:     Alwen Tiu, Tjark Weber
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     3
    Copyright   2005
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     4
49989
34d0ac1bdac6 moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong
blanchet
parents: 49985
diff changeset
     5
Basic setup for the 'sat' and 'satx' tactics.
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     6
*)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     7
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     8
header {* Reconstructing external resolution proofs for propositional logic *}
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     9
26521
f8c4e79db153 tuned imports
haftmann
parents: 21588
diff changeset
    10
theory SAT
49989
34d0ac1bdac6 moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong
blanchet
parents: 49985
diff changeset
    11
imports HOL
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    12
begin
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    13
49989
34d0ac1bdac6 moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong
blanchet
parents: 49985
diff changeset
    14
ML_file "Tools/prop_logic.ML"
34d0ac1bdac6 moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong
blanchet
parents: 49985
diff changeset
    15
ML_file "Tools/sat_solver.ML"
55239
97921d23ebe3 more standard file/module names;
wenzelm
parents: 49989
diff changeset
    16
ML_file "Tools/sat.ML"
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46096
diff changeset
    17
55239
97921d23ebe3 more standard file/module names;
wenzelm
parents: 49989
diff changeset
    18
method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o SAT.sat_tac) *}
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    19
  "SAT solver"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    20
55239
97921d23ebe3 more standard file/module names;
wenzelm
parents: 49989
diff changeset
    21
method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o SAT.satx_tac) *}
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    22
  "SAT solver (with definitional CNF)"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    23
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    24
end