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:
   • $\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.
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}\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})\}$

Referências

• «LABRA, José E., et al., Lógica Proposicional para Informática; Acessado em 17 de dezembro de 2006» (PDF) (em espanhol) 
• «MOREIRA, Nelma; Lógica Computacional; Acessado em 17 de dezembro de 2006» (PDF) 
• «OLIVEIRA, Alcione de Paiva, et al., Introdução à Lógica Matemática para Ciência da Computação; Acessado em 17 de dezembro de 2006» (PDF) 
• «RINCÓN, Mauricio Ayala; Fundamentos da Programação Lógica e Funcional - O Princípio da Resolução e a Teoria da Escrita; Acessado em 17 de dezembro de 2006» (PDF) 

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