Negationsnormalform

Eine logische Formel ist in Negationsnormalform (NNF), falls die Negationsoperatoren in ihr nur direkt über atomaren Aussagen vorkommen.

Eine Formel in Negationsnormalform kann in die konjunktive (KNF) oder disjunktive Normalform (DNF) gebracht werden, indem man die Distributivgesetze anwendet.

Im Allgemeinen gibt es für jede aussagenlogische Formel mehr als eine Negationsnormalform. Das kann man sich veranschaulichen, indem man sich vor Augen führt, dass jede konjunktive und jede disjunktive Normalform zugleich auch eine Negationsnormalform ist.

Vorgehensweise

In klassischer Logik kann jede Formel in diese Form gebracht werden, indem man wie folgt vorgeht:

• Man löst die in ihr vorkommenden materialen Implikationen und Bikonditionale mittels der für diese geltenden Äquivalenzgesetze auf. Beispiele sind (Siehe dazu auch: Implikation):
  • ${\displaystyle P\rightarrow Q\equiv \neg P\lor Q}$
  • ${\displaystyle \neg (P\rightarrow Q)\equiv P\land \neg Q}$
  • ${\displaystyle P\leftrightarrow Q\equiv (P\land Q)\lor (\neg P\land \neg Q)}$
• Man verschiebt mittels der De Morganschen Gesetze die Negationen nach innen und beseitigt dabei zugleich gegebenenfalls auftretende doppelte Negationen

Beispiel

Gegeben sei die folgende Formel:
${\displaystyle \neg (A\rightarrow (B\wedge \neg (C\vee D)))}$

Die Formel ist nicht in NNF, weil Negationen vor nichtatomaren Teilformeln auftreten. Dies ist sowohl vor der äußeren Klammer als auch innerhalb (vor ${\displaystyle (C\vee D)}$) der Fall. Daher zieht man die Negation nach innen und formt um:
${\displaystyle \neg (A\rightarrow (B\wedge \neg (C\vee D)))\equiv (A\wedge \neg (B\wedge \neg (C\vee D)))}$

Da auch in dieser Formel noch komplexe Formeln verneint sind, wird weiter umgeformt:
${\displaystyle (A\wedge (\neg B\vee \neg \neg (C\vee D)))}$

Nun ist noch die hierbei aufgetretene doppelte Negation zu beseitigen:
${\displaystyle (A\wedge (\neg B\vee (C\vee D)))}$

Damit ist die NNF erreicht, weil ${\displaystyle \neg }$ nur noch vor atomaren Teilformeln (d. h. Variablen) auftritt.