Forma normal clausal
# Forma normal clausal

A forma normal clausal é usada em programação lógica e em muitos sistemas provadores de teoremas. O procedimento de conversão de uma fórmula para a forma clausal pode destruir a estrutura da fórmula e, além disso, traduções feitas de forma descuidada freqüentemente causam o crescimento exponencial no tamanho da fórmula resultante.
O procedimento começa com uma fórmula qualquer da lógica clássica de primeira ordem:
* Coloque a fórmula na forma normal prenex.
* Realize o fecho universal da fórmula.
* Skolemize - substitua as variáveis existenciais por constantes de Skolem ou funções de Skolem de variáveis universais, de fora para dentro. Faça as seguintes substituições:
** $\exists x.P(x)$ torna-se $P(c)$, onde $c$ é novo.
** $\forall x....\exists y.P(y)$ torna-se $\forall x....P(f_{c}(x))$, onde $f_{c}$ é nova.
* Remova os quantificadores universais.
* Coloque a fórmula na forma normal conjuntiva.
* Coloque a sentença resultante na forma de um conjunto de cláusulas, substituindo $C_{1}\land ...\land C_{n}$ por $\{C_{1},...,C_{n}\}$.
Freqüentemente, é suficiente gerar uma FNC eqüi-satisfatível (não uma equivalente) para uma fórmula. Nesse caso, o pior caso de crescimento exponencial pode ser evitado introduzindo definições e usando-as para renomear partes da fórmula.

## Exemplos

Exemplo 1: $\forall x(\exists z(\lnot P(x,z)\lor \exists yP(y,x))$
Passo 1) A fórmula já está na forma normal prenex.
Passo 2) Skolemizar a fórmula:
             $\forall x\exists z\exists y(\lnot P(x,z)\lor P(y,x))$
Substituindo $z$ por $f(x)$ e $y$ por $g(x):$
             $\forall x(\lnot P(x,f(x))\lor P(g(x),x))$
Passo 3) Remover o quantificador universal $\forall x$:
             $\lnot P(x,f(x))\lor P(g(x),x)$
Passo 4) A fórmula já está na forma norma conjuntiva.
Passo 5) Olhando para isto como um conjunto de cláusulas:
             $\{\lnot P(x,f(x))\lor P(g(x),x)\}$
Exemplo 2: $\forall x(\lnot \forall y(P(x,y)\land \forall z\lnot R(y,z))\land \forall y\lnot P(x,y))$
Passo 1) Colocar a fórmula na forma normal da negação:
             $\forall x(\lnot \forall y(P(x,y)\land \forall z\lnot R(y,z))\land \forall y\lnot P(x,y))$
             $\forall x(\exists y\lnot (P(x,y)\land \forall z\lnot R(y,z))\land \forall y\lnot P(x,y))$
             $\forall x(\exists y(\lnot P(x,y)\lor \lnot \forall z\lnot R(y,z))\land \forall y\lnot P(x,y))$
             $\forall x(\exists y(\lnot P(x,y)\lor \exists zR(y,z))\land \forall y\lnot P(x,y))$
Passo 2) Skolemizar a fórmula:
             $\forall x\exists y_{1}\exists z\forall y_{2}((\lnot P(x,y_{1})\lor R(y_{1},z))\land \lnot P(x,y_{2}))$
Substituindo $y_{1}$ por $f(x)$ e $z$ por $g(x)$:
             $\forall x\forall y_{2}((\lnot P(x,f(x))\lor R(f(x),g(x))\land \lnot P(x,y_{2}))$
Passo 3) Remover os quantificadores universais $\forall x$ e $\forall y_{2}$:
             $((\lnot P(x,f(x))\lor R(f(x),g(x))\land \lnot P(x,y_{2}))$
Passo 4) A fórmula já está na forma normal conjuntiva.
Passo 5) Dispor na forma de um conjunto de cláusulas:
             $\{\lnot P(x,f(x))\lor R(f(x),g(x)),\lnot P(x,y_{2})\}$