Editing Conjunctive normal form (section)

==== Conversion by syntactic means ====
Convert to CNF the propositional formula <math>\phi</math>.

'''Step 1''': Convert its negation to disjunctive normal form.<ref name="dnf">see {{slink|Disjunctive normal form#Conversion to DNF}}</ref> 

<math>\lnot \phi_{DNF} = (C_1 \lor C_2 \lor \ldots \lor C_i \lor \ldots \lor C_m)</math>,{{refn|<math>1 \le m \le</math> [[Disjunctive normal form#max_conjunctions|maximum number of conjunctions]] for <math>\phi</math>}}

where each <math>C_i</math> is a conjunction of literals <math>l_{i1} \land l_{i2} \land \ldots \land l_{in_i}</math>.{{refn|<math>1 \le in_i \le</math> [[Disjunctive normal form#max conjunctions|maximum number of literals]] for <math>\phi</math>}}

'''Step 2''': Negate <math>\lnot \phi_{DNF}</math>.
Then shift <math>\lnot</math> inwards by applying the [[De Morgan's laws#Formal notation|(generalized) De Morgan's equivalences]] until no longer possible.
<math display="block">\begin{align}
\phi &\leftrightarrow \lnot \lnot \phi_{DNF} \\
&= \lnot (C_1 \lor C_2 \lor \ldots \lor C_i \lor \ldots \lor C_m) \\
&\leftrightarrow \lnot C_1 \land \lnot C_2 \land \ldots \land \lnot C_i \land \ldots \land \lnot C_m &&\text{// (generalized) D.M.} 
\end{align}</math>
where<math display="block">\begin{align}
\lnot C_i &= \lnot (l_{i1} \land l_{i2} \land \ldots \land l_{in_i}) \\
&\leftrightarrow (\lnot l_{i1} \lor \lnot l_{i2} \lor \ldots \lor \lnot l_{in_i}) &&\text{// (generalized) D.M.}
\end{align}</math>

'''Step 3''': Remove all double negations.

'''Example'''

Convert to CNF the propositional formula
<math>\phi = ((\lnot (p \land q)) \leftrightarrow (\lnot r \uparrow (p \oplus q)))</math>.{{refn|name=phiverbose|1=<math>\phi</math> = (('''[[Negation|NOT]]''' (p '''[[Logical conjunction|AND]]''' q)) '''[[If and only if|IFF]]''' (('''[[Negation|NOT]]''' r) '''[[Sheffer stroke|NAND]]''' (p '''[[XOR]]''' q)))}}

The (full) DNF equivalent of its negation is<ref name="dnf" /><br/>
<math> \lnot \phi_{DNF} =
(      p \land       q \land       r) \lor
(      p \land       q \land \lnot r) \lor
(      p \land \lnot q \land \lnot r) \lor
(\lnot p \land       q \land \lnot r) </math>

<math display="block">\begin{align}
\phi &\leftrightarrow \lnot \lnot \phi_{DNF} \\
&= \lnot \{
(      p \land       q \land       r) \lor
(      p \land       q \land \lnot r) \lor
(      p \land \lnot q \land \lnot r) \lor
(\lnot p \land       q \land \lnot r) \} \\
&\leftrightarrow
\underline{\lnot( p \land       q \land       r)} \land
\underline{\lnot( p \land       q \land \lnot r)} \land
\underline{\lnot( p \land \lnot q \land \lnot r)} \land
\underline{\lnot(\lnot p  \land q \land \lnot r)} &&\text{// generalized D.M. } \\
&\leftrightarrow
(\lnot p \lor  \lnot q \lor \lnot r) \land
(\lnot p \lor  \lnot q \lor \lnot \lnot r) \land
(\lnot p \lor \lnot \lnot q \lor \lnot \lnot r) \land
(\lnot \lnot p \lor \lnot q \lor \lnot \lnot r) &&\text{// generalized D.M. } (4 \times) \\
&\leftrightarrow
(\lnot p \lor  \lnot q \lor \lnot r) \land
(\lnot p \lor  \lnot q \lor       r) \land
(\lnot p \lor        q \lor       r) \land
(      p \lor \lnot q \lor        r) &&\text{// remove all } \lnot \lnot \\
&= \phi_{CNF}
\end{align}</math>