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:
   • ${\displaystyle \exists x.P(x)}$ torna-se ${\displaystyle P(c)}$, onde ${\displaystyle c}$ é novo.
   • ${\displaystyle \forall x....\exists y.P(y)}$ torna-se ${\displaystyle \forall x....P(f_{c}(x))}$, onde ${\displaystyle 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 ${\displaystyle C_{1}\land ...\land C_{n}}$ por ${\displaystyle \{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: ${\displaystyle \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:

${\displaystyle \forall x\exists z\exists y(\lnot P(x,z)\lor P(y,x))}$

Substituindo ${\displaystyle z}$ por ${\displaystyle f(x)}$ e ${\displaystyle y}$ por ${\displaystyle g(x):}$

${\displaystyle \forall x(\lnot P(x,f(x))\lor P(g(x),x))}$

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

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

${\displaystyle \{\lnot P(x,f(x))\lor P(g(x),x)\}}$

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

${\displaystyle \forall x(\lnot \forall y(P(x,y)\land \forall z\lnot R(y,z))\land \forall y\lnot P(x,y))}$

${\displaystyle \forall x(\exists y\lnot (P(x,y)\land \forall z\lnot R(y,z))\land \forall y\lnot P(x,y))}$

${\displaystyle \forall x(\exists y(\lnot P(x,y)\lor \lnot \forall z\lnot R(y,z))\land \forall y\lnot P(x,y))}$

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

${\displaystyle \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 ${\displaystyle y_{1}}$ por ${\displaystyle f(x)}$ e ${\displaystyle z}$ por ${\displaystyle g(x)}$:

${\displaystyle \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 ${\displaystyle \forall x}$ e ${\displaystyle \forall y_{2}}$:

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

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

• Portal da matemática