Forma normal clausal

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

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:
    • torna-se , onde é novo.
    • torna-se , onde é 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 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[editar | editar código-fonte]

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[editar | editar código-fonte]

Ver também[editar | editar código-fonte]

Wikilivros
O Wikilivros tem um livro chamado Lógica