Negation Normal Form (First-Order Logic)

first-order-logic

Definition

Negation Normal Form (First-Order Logic)

A formula is in negation normal form (NNF) if the only Boolean connectives are $\neg ,\wedge ,\vee$ and every occurrence of $\neg$ appears directly in front of an atomic formula.

Examples

In NNF

$$\neg P(x)\wedge Q(x),\forall x(P(x)\vee \neg Q(x)),P(x)\vee (\neg Q(x)\wedge R(x))$$

Not in NNF

$$\neg (P(x)\wedge Q(x))\text{(negation over ∧)},P(x)\to Q(x)\text{(contains →)},\neg \forall xP(x)\text{(negation over quantifier)}$$