Quiz. Negation Normal Form (NNF) [000f]

unsatisfiability: \(F\) is unsatisfiable if and only if \(F'\) is unsatisfiable.
model correspondence: For every satisfying assignment (model) of \(F'\), there exists a corresponding satisfying assignment of \(F\), and vice versa, when restricted to the original variables of \(F\).

Which of the following formulas are in Negation Normal Form (NNF)?

Solution.

No. The implication operator \(\to \) is not allowed in NNF.
Yes. Negations are only applied to literals, and only \(\land \) and \(\lor \) are used.
No. The negation operator \(\neg \) is applied to a non-literal formula \((\neg r \land s)\).
No. The double negation \(\neg \neg r\) is not allowed in NNF. Important to remember since that can trip you up.