Negationsnormalform

Eine Formel $\phi \in AL$ ist in Negationsnormalform (NNF), wenn die Symbole $\to$ und $\leftrightarrow$ nicht vorkommen und die Negation $\neg$ nur direkt vor atomaren Formeln (Aussagenvariablen) auftritt.