Definition. Negation Normal Form (NNF) [000e]

A formula \(F\) is in Negation Normal Form (NNF) if the negation operator \(\neg \) is only applied to literals (i.e., propositional variables or their negations), and the only other allowed operators are conjunction \(\land \) and disjunction \(\lor \). A nice way to think about it is that we can never have the case where we need to apply De Morgan's laws to push negations further down the formula tree. So all negations come pre-distributed to the literals.