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

Exemplo 1: ∀ x ( ∃ z ( ¬ P ( x , z ) ∨ ∃ y P ( y , x ) ) {\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:

∀ x ∃ z ∃ y ( ¬ P ( x , z ) ∨ P ( y , x ) ) {\displaystyle \forall x\exists z\exists y(\lnot P(x,z)\lor P(y,x))}

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

∀ x ( ¬ P ( x , f ( x ) ) ∨ P ( g ( x ) , x ) ) {\displaystyle \forall x(\lnot P(x,f(x))\lor P(g(x),x))}

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

¬ P ( x , f ( x ) ) ∨ P ( g ( x ) , 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:

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

Exemplo 2: ∀ x ( ¬ ∀ y ( P ( x , y ) ∧ ∀ z ¬ R ( y , z ) ) ∧ ∀ y ¬ P ( x , y ) ) {\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:

∀ x ( ¬ ∀ y ( P ( x , y ) ∧ ∀ z ¬ R ( y , z ) ) ∧ ∀ y ¬ P ( x , y ) ) {\displaystyle \forall x(\lnot \forall y(P(x,y)\land \forall z\lnot R(y,z))\land \forall y\lnot P(x,y))}

∀ x ( ∃ y ¬ ( P ( x , y ) ∧ ∀ z ¬ R ( y , z ) ) ∧ ∀ y ¬ 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))}

∀ x ( ∃ y ( ¬ P ( x , y ) ∨ ¬ ∀ z ¬ R ( y , z ) ) ∧ ∀ y ¬ 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))}

∀ x ( ∃ y ( ¬ P ( x , y ) ∨ ∃ z R ( y , z ) ) ∧ ∀ y ¬ 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:

∀ x ∃ y 1 ∃ z ∀ y 2 ( ( ¬ P ( x , y 1 ) ∨ R ( y 1 , z ) ) ∧ ¬ P ( x , y 2 ) ) {\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 y 1 {\displaystyle y_{1}} por f ( x ) {\displaystyle f(x)} e z {\displaystyle z} por g ( x ) {\displaystyle g(x)} :

∀ x ∀ y 2 ( ( ¬ P ( x , f ( x ) ) ∨ R ( f ( x ) , g ( x ) ) ∧ ¬ P ( x , y 2 ) ) {\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 ∀ x {\displaystyle \forall x} e ∀ y 2 {\displaystyle \forall y_{2}} :

( ( ¬ P ( x , f ( x ) ) ∨ R ( f ( x ) , g ( x ) ) ∧ ¬ P ( x , 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:

{ ¬ P ( x , f ( x ) ) ∨ R ( f ( x ) , g ( x ) ) , ¬ P ( x , y 2 ) } {\displaystyle \{\lnot P(x,f(x))\lor R(f(x),g(x)),\lnot P(x,y_{2})\}}

• «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) 

• 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