Forma normal da negação

Uma fórmula lógica está na forma normal da negação se a negação ocorre logo após fórmulas atômicas, e {${\displaystyle \lnot ,\lor ,\land }$} são os únicos conectivos booleanos permitidos. Na lógica clássica, cada fórmula pode ser convertida para essa forma substituindo implicações e equivalências pelas suas definições, usando as leis de De Morgan para internalizar a negação na fórmula e eliminando duplas negações. Esse processo pode ser representado através das seguintes regras de conversão:

${\displaystyle \lnot (\forall x.G)\twoheadrightarrow \exists x.\lnot G}$

${\displaystyle \lnot (\exists x.G)\twoheadrightarrow \forall x.\lnot G}$

${\displaystyle \lnot \lnot G\twoheadrightarrow G}$

${\displaystyle \lnot (G_{1}\land G_{2})\twoheadrightarrow (\lnot G_{1})\lor (\lnot G_{2})}$

${\displaystyle \lnot (G_{1}\lor G_{2})\twoheadrightarrow (\lnot G_{1})\land (\lnot G_{2})}$

Uma fórmula na forma normal da negação pode ser colocada numa forma mais forte, como a forma normal conjuntiva ou a forma normal disjuntiva aplicando as leis da distributividade.