Converts a term already in negation normal form into conjunctive normal form.
DESCRIPTION
When applied to a term already in negation normal form (see NNF_CONV),
meaning that all other propositional connectives have been eliminated in favour
of conjunction, disjunction and negation, and negation is only applied to
atomic formulas, CNF_CONV puts the term into an equivalent conjunctive normal
form, which is a right-associated conjunction of disjunctions without
repetitions. No reduction by subsumption is performed, however, e.g. from
a /\ (a \/ b) to just a).
FAILURE CONDITIONS
Never fails; non-Boolean terms will just yield a reflexive theorem.
EXAMPLE
# CNF_CONV `(a /\ b) \/ (a /\ b /\ c) \/ d`;;
val it : thm =
|- a /\ b \/ a /\ b /\ c \/ d <=>
(a \/ d) /\ (a \/ b \/ d) /\ (a \/ c \/ d) /\ (b \/ d) /\ (b \/ c \/ d)