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 , onde é novo. torna-se , onde é 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 .
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:
Passo 1) A fórmula já está na forma normal prenex.
Passo 2) Skolemizar a fórmula:
Substituindo por e por
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 por e por :
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:
Referências
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
Categoria:Lógica matemática