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

Exemplo 1:  \forall x (\exists z (\lnot P(x,z) \lor \exists y P(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 z R(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[editar | editar código-fonte]

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

Wikilivros
O Wikilivros tem um livro chamado Lógica