Negation normal form

A propositional formula is in negation normal form if it is in boolean normal form and negation only occurs in front of variables. Negation normal form is a simple normal form, which is used when it is important to control the occurrence of negation, for instance, when it is important to avoid the negation of larger subformulas. Every propositional formula is equivalent to a formula in negation normal form.

Formal Definition

The set of propositional formulas in negation normal form (NNF) is defined inductively as follows.

Base set.

• $\top$ and $\bot$ are in NNF.
• For every $i$, the formula $X_i$ and the formula $\neg X_i$ are in NNF.

Inductive rule.

• If $\varphi$ and $\psi$ are in NNF, then $\varphi \vee \psi$ and $\varphi \wedge \psi$ are in NNF.

In other words, the set of connectives is restricted to the ones which are typically used for calculating with truth values, that is, to $\vee$, $\wedge$, and $\neg$. In addition, $\neg$ may only occur in front of a variable.

Example The formula $X_0 \wedge (\neg X_1 \vee X_0)$ is in NNF, whereas neither $X_0 \wedge (\neg\neg X_1 \vee X_0)$ nor $X_0 \wedge (\neg\neg X_1 \rightarrow X_0)$ nor $\neg (X_0 \wedge (\neg\neg X_1 \vee X_0))$ are in NNF.

Negation of formulas in NNF

An important property of formulas in NNF is that negation only occurs in front of variables. Still, it is fairly simple to negate a formula in NNF. Because of de Morgan's laws (demo), the law of double negation (done) and because of the law of duality (dual), the only thing one needs to do is to interchange $\vee$ and $\wedge$ as well as negated and non-negated variables (and accordingly $\bot$ and $\top$).

Here is an algorithm that exactly does this:

  NegNNF($\varphi$)
  Precondition: $\varphi$ is in NNF
  case $\varphi$ of
    $\bot$: return $\top$
    $\top$: return $\bot$
    $X_i$: return $\neg X_i$
    $\neg X_i$: return $X_i$
    $\varphi_0 \vee \varphi_1$: return NegNNF($\varphi_0$) $\wedge$ NegNNF($\varphi_1$)
    $\varphi_0 \wedge \varphi_1$: return NegNNF($\varphi_0$) $\vee$ NegNNF($\varphi_1$)
  Postcondition: return is equivalent to $\neg \varphi$ and in NNF

Example We have \begin{align*} \text{NegNNF}(\neg X_2 \wedge (\neg X_0 \vee X_1)) & = \text{NegNNF}(\neg X_2) \vee \text{NegNNF}(\neg X_0 \vee X_1)\\ & = X_2 \vee (\text{NegNNF}(\neg X_0) \wedge \text{NegNNF}(X_1))\\ & = X_2 \vee (X_0 \wedge \neg X_1) \end{align*}

Conversion into negation normal form

There is a fairly simple algorithm that turns a formula in boolean normal form into negation normal form: if a negation occurs, the algorithm is applied recursively to the non-negated formula and NegNNF is applied to the result.

  BNF2NNF($\varphi$)
  Precondition: $\varphi$ is in BNF
  case $\varphi$ of
    $\bot$: return $\bot$
    $\top$: return $\top$
    $X_i$: return $X_i$
    $\neg \varphi_0$: NegNNF(BNF2NNF$(\varphi_0))$
    $\varphi_0 \vee \varphi_1$: return BNF2NNF($\varphi_0$) $\vee$ BNF2NNF($\varphi_1$)
    $\varphi_0 \wedge \varphi_1$: return BNF2NNF($\varphi_0$) $\wedge$ BNF2NNF($\varphi_1$)
  Postcondition: return is equivalent to $\varphi$ and in NNF

Example We have \begin{align*} \text{BNF2NNF}(\neg(\neg X_2 \wedge (\neg X_0 \vee X_1))) & = \text{NegNNF}(\text{BNF2NNF}(\neg X_2 \wedge (\neg X_0 \vee X_1))\\ & = \text{NegNNF}(\text{BNF2NNF}(\neg X_2) \wedge \text{BNF2NNF}(\neg X_0 \vee X_1))\\ & = \text{NegNNF}(\text{NegNNF}(\text{BNF2NNF}(X_2)) \wedge (\text{BNF2NNF}(\neg X_0) \vee \text{BNF2NNF}(X_1))\\ & = \text{NegNNF}(\text{NegNNF}(X_2) \wedge (\text{NegNNF}(\text{BNF2NNF}(X_0)) \vee X_1))\\ & = \text{NegNNF}(\neg X_2 \wedge (\text{NegNNF}(X_0) \vee X_1))\\ & = \text{NegNNF}(\neg X_2 \wedge (\neg X_0 \vee X_1))\\ & = \text{NegNNF}(\neg X_2) \vee \text{NegNNF}(\neg X_0 \vee X_1)\\ & = X_2 \vee (\text{NegNNF}(\neg X_0) \wedge \text{NegNNF}(X_1))\\ & = X_2 \vee (X_0 \wedge \neg X_1) \end{align*}

Theorem Every propositional formula is equivalent to a formula in negation normal form.

To prove this, one only needs to combine the above algorithm with the algorithm for converting an arbitrary propositional formula into a formula in boolean normal form.

Alternative conversion

Instead of using NegNNF, one could also make use of de Morgan's laws to convert a formula in BNF into NNF. This leads, in a natural fashion to two recursive procedures: one that converts a formula into NNF, another one which converts the negation of a formula into NNF.

  BNF2NNF2($\varphi$)
  Precondition: $\varphi$ is in BNF
  case $\varphi$ of
    $\bot$: return $\bot$
    $\top$: return $\top$
    $X_i$: return $X_i$
    $\neg \varphi_0$: BNF2NNF2-neg$(\varphi_0)$
    $\varphi_0 \vee \varphi_1$: return BNF2NNF2($\varphi_0$) $\vee$ BNF2NNF2($\varphi_1$)
    $\varphi_0 \wedge \varphi_1$: return BNF2NNF2($\varphi_0$) $\wedge$ BNF2NNF2($\varphi_1$)
  Postcondition: return is equivalent to $\varphi$ and in NNF

  BNF2NNF2-neg($\varphi$)
  Precondition: $\varphi$ is in BNF
  case $\varphi$ of
    $\bot$: return $\top$
    $\top$: return $\bot$
    $X_i$: return $\neg X_i$
    $\neg \varphi_0$: BNF2NNF2$(\varphi_0)$
    $\varphi_0 \vee \varphi_1$: return BNF2NNF2-neg($\varphi_0$) $\wedge$ BNF2NNF2-neg($\varphi_1$)
    $\varphi_0 \wedge \varphi_1$: return BNF2NNF2-neg($\varphi_0$) $\vee$ BNF2NNF2-neg($\varphi_1$)
  Postcondition: return is equivalent to $\neg \varphi$ and in NNF