Formula je u negacionoj normalnoj formi akko je izgrađena od literala korišćenjem veznika ∧, ∨ i kvantifikatora.
Pri svođenju formule na NNF koriste se logički zakoni iz iskazne logike (asocijativnost, komutativnost, dvostruka negacija itd.), a mogu da se koriste i pravila navedena u 3 Pravila transformaciije