Forma normal clausal: diferenças entre revisões

 

#Coloque a fórmula na [[Forma normal negativa|Forma Normal Negativa]];

#[[Skolemização|Skolemize]] - substitua as variáveis existenciais por constantes de [[Thoralf Skolem|Skolem]] ou funções de Skolem de variáveis universais, de fora para dentro. Faça as seguintes substituições:

#* <math>\exists x. P(x)</math> torna-se '''P(c)''', onde c é novo.

#* <math>\forall x. ... \exists y. P(y)</math> torna-se <math>\forall x. ... P(f_c(x))</math>, onde <math>f_c</math> é nova.

#Remova os quantificadores universais

#Coloque a fórmula na [[Forma normal conjuntiva|Forma Normal Conjuntiva]].

# Substitua <math>C1 \wedge ... \wedge Cn</math> por <math>\{C1 , ... , Cn\}</math>. Cada conjunto é da forma <math>\neg A1 \vee ... \vee \neg Am \vee B1 \vee ... \vee Bn</math>, que é equivalente à <math>( A1 \wedge ... \wedge Am ) \to ( B1 \vee ... \vee Bn )</math>.

#* Se m=0 e n=1, isto é um fato do [[Prolog]].

#* Se m>0 e n=1, isto é uma regra do Prolog.

#* Se m>0 e n=0, isto é uma consulta do Prolog.

# Finalmente, substitua cada [[Conjunto|conjunto]] <math>( A1 \wedge ... \wedge Am ) \to ( B1 \vee ... \vee Bn )</math> por <math>\{ A1 \wedge ... \wedge Am \to B1 , A1 \wedge ... \wedge Am \to B2 , ... , A1 \wedge ... \wedge Am \to Bn \}</math>.

Quando n=1, a lógica é chamda de lógica da [[Cláusula de Horn|cláusula de Horn]] e é equivalente, do ponto de vista do poder computacional, à [[Máquina de Turing universal]].