Negation normal form

In mathematical logic, a formula is in negation normal form (NNF) if the negation operator (${\displaystyle \lnot }$, not) is only applied to variables and the only other allowed Boolean operators are conjunction (${\displaystyle \land }$, and) and disjunction (${\displaystyle \lor }$, or).

Negation normal form is not a canonical form: for example, ${\displaystyle a\land (b\lor \lnot c)}$ and ${\displaystyle (a\land b)\lor (a\land \lnot c)}$ are equivalent, and are both in negation normal form.