This is an old revision of the document!

Normal Forms for Propositional Logic

Negation-Normal Form

In Negation-normal from, negations are only allowed on elementary proposition. Moreover, NNF formulas contain no implication, so the only binary operators are conjunctions and disjunctions. The following rules can be used to turn arbitrary propositional formulas into negation-normal form. \[\begin{array}{l}

\lnot (p \land q) \leftrightarrow (\lnot p) \lor (\lnot q) \\
p \leftrightarrow  \lnot (\lnot p) \\
(p \rightarrow q) \leftrightarrow ((\lnot p) \lor q) \\
\lnot (p \lor q) \leftrightarrow (\lnot p) \land (\lnot q)

\end{array} \] Note that this transformation is linear in the size of the formula. No exponential blow-up.

Recall homework01.

Polarity of formula.

Disjunctive Normal Form

Formulas in Disjunctive-normal form look like this: $(x_1 \land x_2 \land \lnot x_3) \lor (\lnot x_1 \land x_3 \land x_4) \lor ...$
More formally $F = \bigvee^{n}_{i=1} D_i$ where $n \geq 0$ .
Each $D_i$ is a clause and is defined as $D_i = \bigwedge_{j=1}^{n_i} L_{ij}$ .
Each $L_{ij}$ is a literal. It's either an elementary proposition or its negation.

Solving the SAT problem for DNF formulas is in P, but transforming an arbitrary propositional formula to DNF causes an exponential blow-up.

DNF formulas can be easily generated from truth tables. Each row of the truth table that makes the formula true can be written as a clause. For a formula over $n$ variables, there are $2^{n}$ rows in the truth table. Over $n$ variables, there are $2^{2^{n}}$ different (i.e. non-equivalent) formulas.

Conjunctive Normal Form

Formulas in Conjunctive-normal form look like this: $(x_1 \lor x_2 \lor \lor x_3) \land (\lnot x_1 \lor x_3 \lor x_4) \land ...$
It's defined as $F = \bigwedge^{n}_{i=1} D_i$ and $D_i = \bigvee_{j=1}^{n_i} L_{ij}$
Like for DNF, $L_{ij}$ are elementary propositions or their negation. The terminology of clauses and literals also applies to CNF.