Forma normal clausal
Origem: Wikipédia, a enciclopédia livre.
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:
torna-se P(c), onde c é novo.
torna-se 
, onde fc é 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
por {C1,...,Cn}.
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.
[editar] Exemplos
Exemplo 1: 
Passo 1) A fórmula já está na forma normal prenex.
Passo 2) Skolemizar a fórmula:
Substituindo z por f(x) e y por g(x):
Passo 3) Remover o quantificador universal 
:
Passo 4) A fórmula já está na forma norma conjuntiva.
Passo 5) Olhando para isto como um conjunto de cláusulas:
Exemplo 2: 
Passo 1) Colocar a fórmula na forma normal da negação:
Passo 2) Skolemizar a fórmula:
Substituindo y1 por f(x) e z por g(x):
Passo 3) Remover os quantificadores universais e 
:
Passo 4) A fórmula já está na forma normal conjuntiva.
Passo 5) Dispor na forma de um conjunto de cláusulas:
[editar] Referências
- LABRA, José E., et al., Lógica Proposicional para Informática; Acessado em 17 de dezembro de 2006 ((es))
