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 {$\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:

$\lnot (\forall x.G)\twoheadrightarrow \exists x.\lnot G$

$\lnot (\exists x.G)\twoheadrightarrow \forall x.\lnot G$

$\lnot \lnot G\twoheadrightarrow G$

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

$\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.

Ver também

• Forma Normal Algébrica
• Forma Normal Conjuntiva
• Forma Normal Disjuntiva
• Cláusula de Horn