In Boolean algebra, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs.

In automated theorem proving, the notion "clausal normal form" is often used in a narrower sense, meaning a particular representation of a CNF formula as a set of sets of literals.

Definition

A logical formula is considered to be in CNF if it is a conjunction of one or more disjunctions of one or more literals. As in disjunctive normal form (DNF), the only propositional operators in CNF are or (<math>\vee</math>), and (<math>\and</math>), and not (<math>\neg</math>). The not operator can only be used as part of a literal, which means that it can only precede a propositional variable.

The following is a context-free grammar for CNF:

: CNF <math>\, \to \,</math> Disjunct <math>\, \mid \, </math> Disjunct <math>\, \land \,</math> CNF

: Disjunct <math>\, \to \,</math> Literal <math>\, \mid\, </math> Literal <math>\, \lor \,</math> Disjunct

: Literal <math>\, \to \,</math> Variable <math>\, \mid \,</math> <math>\, \neg \,</math> Variable

Where Variable is any variable.

All of the following formulas in the variables <math>A,B,C,D,E,</math> and <math>F</math> are in conjunctive normal form:

  • <math>(A \lor \neg B \lor \neg C) \land (\neg D \lor E \lor F)</math>
  • <math>(A \lor B) \land (C)</math>
  • <math>(A \lor B)</math>
  • <math>(A)</math>

The following formulas are not in conjunctive normal form:

  • <math>\neg (A \land B)</math>, since an AND is nested within a NOT
  • <math>\neg(A \lor B) \land C</math>, since an OR is nested within a NOT
  • <math>A \land (B \lor (D \land E))</math>, since an AND is nested within an OR
  • <math>A\land(B\lor(C\lor D))</math>, since a nested OR should be written without parenthesis

Conversion to CNF

In classical logic each propositional formula can be converted to an equivalent formula that is in CNF. This transformation is based on rules about logical equivalences: double negation elimination, De Morgan's laws, and the distributive law.

Basic algorithm

The algorithm to compute a CNF-equivalent of a given propositional formula <math>\phi</math> builds upon <math>\lnot \phi</math> in disjunctive normal form (DNF): step 1.

<math>\lnot \phi_{DNF} = (C_1 \lor C_2 \lor \ldots \lor C_i \lor \ldots \lor C_m)</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>.

Step 2: Negate <math>\lnot \phi_{DNF}</math>.

Then shift <math>\lnot</math> inwards by applying the (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>.

The (full) DNF equivalent of its negation is