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