src/HOL/Tools/cnf_funcs.ML
changeset 32960 69916a850301
parent 32740 9dd0a2f83429
child 33035 15eab423e573
     1.1 --- a/src/HOL/Tools/cnf_funcs.ML	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -2,33 +2,34 @@
     1.4      Author:     Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
     1.5      Author:     Tjark Weber, TU Muenchen
     1.6  
     1.7 -  FIXME: major overlaps with the code in meson.ML
     1.8 +FIXME: major overlaps with the code in meson.ML
     1.9 +
    1.10 +Functions and tactics to transform a formula into Conjunctive Normal
    1.11 +Form (CNF).
    1.12  
    1.13 -  Description:
    1.14 -  This file contains functions and tactics to transform a formula into
    1.15 -  Conjunctive Normal Form (CNF).
    1.16 -  A formula in CNF is of the following form:
    1.17 +A formula in CNF is of the following form:
    1.18  
    1.19 -      (x11 | x12 | ... | x1n) & ... & (xm1 | xm2 | ... | xmk)
    1.20 -      False
    1.21 -      True
    1.22 +    (x11 | x12 | ... | x1n) & ... & (xm1 | xm2 | ... | xmk)
    1.23 +    False
    1.24 +    True
    1.25  
    1.26 -  where each xij is a literal (a positive or negative atomic Boolean term),
    1.27 -  i.e. the formula is a conjunction of disjunctions of literals, or
    1.28 -  "False", or "True".
    1.29 +where each xij is a literal (a positive or negative atomic Boolean
    1.30 +term), i.e. the formula is a conjunction of disjunctions of literals,
    1.31 +or "False", or "True".
    1.32  
    1.33 -  A (non-empty) disjunction of literals is referred to as "clause".
    1.34 +A (non-empty) disjunction of literals is referred to as "clause".
    1.35  
    1.36 -  For the purpose of SAT proof reconstruction, we also make use of another
    1.37 -  representation of clauses, which we call the "raw clauses".
    1.38 -  Raw clauses are of the form
    1.39 +For the purpose of SAT proof reconstruction, we also make use of
    1.40 +another representation of clauses, which we call the "raw clauses".
    1.41 +Raw clauses are of the form
    1.42 +
    1.43 +    [..., x1', x2', ..., xn'] |- False ,
    1.44  
    1.45 -      [..., x1', x2', ..., xn'] |- False ,
    1.46 +where each xi is a literal, and each xi' is the negation normal form
    1.47 +of ~xi.
    1.48  
    1.49 -  where each xi is a literal, and each xi' is the negation normal form of ~xi.
    1.50 -
    1.51 -  Literals are successively removed from the hyps of raw clauses by resolution
    1.52 -  during SAT proof reconstruction.
    1.53 +Literals are successively removed from the hyps of raw clauses by
    1.54 +resolution during SAT proof reconstruction.
    1.55  *)
    1.56  
    1.57  signature CNF =