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:

1. Coloque a fórmula na forma normal prenex.
2. Realize o fecho universal da fórmula.
3. 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:
   • $\mathrm{\exists }x.P(x)$ torna-se $P(c)$, onde $c$ é novo.
   • $\mathrm{\forall }x....\mathrm{\exists }y.P(y)$ torna-se $\mathrm{\forall }x....P(f_c(x))$, onde $f_c$ é nova.
4. Remova os quantificadores universais.
5. Coloque a fórmula na forma normal conjuntiva.
6. Coloque a sentença resultante na forma de um conjunto de cláusulas, substituindo $C_1\wedge ...\wedge 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: $\mathrm{\forall }x(\mathrm{\exists }z(\mathrm{\neg }P(x,z)\vee \mathrm{\exists }yP(y,x))$

Passo 1) A fórmula já está na forma normal prenex.

Passo 2) Skolemizar a fórmula:

$\mathrm{\forall }x\mathrm{\exists }z\mathrm{\exists }y(\mathrm{\neg }P(x,z)\vee P(y,x))$

Substituindo $z$ por $f(x)$ e $y$ por $g(x):$

$\mathrm{\forall }x(\mathrm{\neg }P(x,f(x))\vee P(g(x),x))$

Passo 3) Remover o quantificador universal $\mathrm{\forall }x$:

$\mathrm{\neg }P(x,f(x))\vee 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:

$\{\mathrm{\neg }P(x,f(x))\vee P(g(x),x)\}$

Exemplo 2: $\mathrm{\forall }x(\mathrm{\neg }\mathrm{\forall }y(P(x,y)\wedge \mathrm{\forall }z\mathrm{\neg }R(y,z))\wedge \mathrm{\forall }y\mathrm{\neg }P(x,y))$

Passo 1) Colocar a fórmula na forma normal da negação:

$\mathrm{\forall }x(\mathrm{\neg }\mathrm{\forall }y(P(x,y)\wedge \mathrm{\forall }z\mathrm{\neg }R(y,z))\wedge \mathrm{\forall }y\mathrm{\neg }P(x,y))$

$\mathrm{\forall }x(\mathrm{\exists }y\mathrm{\neg }(P(x,y)\wedge \mathrm{\forall }z\mathrm{\neg }R(y,z))\wedge \mathrm{\forall }y\mathrm{\neg }P(x,y))$

$\mathrm{\forall }x(\mathrm{\exists }y(\mathrm{\neg }P(x,y)\vee \mathrm{\neg }\mathrm{\forall }z\mathrm{\neg }R(y,z))\wedge \mathrm{\forall }y\mathrm{\neg }P(x,y))$

$\mathrm{\forall }x(\mathrm{\exists }y(\mathrm{\neg }P(x,y)\vee \mathrm{\exists }zR(y,z))\wedge \mathrm{\forall }y\mathrm{\neg }P(x,y))$

Passo 2) Skolemizar a fórmula:

$\mathrm{\forall }x\mathrm{\exists }{y}_1\mathrm{\exists }z\mathrm{\forall }{y}_2((\mathrm{\neg }P(x,y_1)\vee R(y_1,z))\wedge \mathrm{\neg }P(x,y_2))$

Substituindo $y_1$ por $f(x)$ e $z$ por $g(x)$:

$\mathrm{\forall }x\mathrm{\forall }{y}_2((\mathrm{\neg }P(x,f(x))\vee R(f(x),g(x))\wedge \mathrm{\neg }P(x,y_2))$

Passo 3) Remover os quantificadores universais $\mathrm{\forall }x$ e $\mathrm{\forall }{y}_2$:

$((\mathrm{\neg }P(x,f(x))\vee R(f(x),g(x))\wedge \mathrm{\neg }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:

$\{\mathrm{\neg }P(x,f(x))\vee R(f(x),g(x)),\mathrm{\neg }P(x,y_2)\}$

Referências

• Predefinição:Link
• Predefinição:Link
• Predefinição:Link
• Predefinição:Link

Ver também

• Cláusula (lógica)
• Cláusula de Horn
• Forma normal prenex
• Lógica
• Princípio da resolução
• Programação lógica
• Prolog
• Unificação