|
#* <math>\exists x. P(x)</math> torna-se <math>P(c)</math>, onde <math>c</math> é 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 [[Quantificação Universal|quantificadores universais]] ([[:en:Universal quantification]]).
#Coloque a fórmula na [[Forma normal conjuntiva|forma normal conjuntiva]].
# SubstituaColoque na forma de cláusulas, substituindo <math>C_1 \wedgeland ... \wedgeland C_n</math> por <math>\{C_1 , ... , C_n\}</math>. Cada conjunto é da forma <math>\neg A_1 \vee ... \vee \neg A_m \vee B_1 \vee ... \vee B_n</math>, que é equivalente à <math>( A_1 \wedge ... \wedge A_m ) \to ( B_1 \vee ... \vee B_n )</math>.
#* Se <math>m=0</math> e <math>n=1</math>, isto é um [[Prolog#Fatos|fato do Prolog]].
#* Se <math>m>0</math> e <math>n=1</math>, isto é uma [[Prolog#Regras|regra do Prolog]].
#* Se <math>m>0</math> e <math>n=0</math>, isto é uma [[Prolog#Avaliação|consulta do Prolog]].
# Finalmente, substitua cada [[Conjunto|conjunto]] <math>( A_1 \wedge ... \wedge A_m ) \to ( B_1 \vee ... \vee B_n )</math> por <math>\{ A_1 \wedge ... \wedge A_m \to B_1 , A_1 \wedge ... \wedge A_m \to B_2 , ... , A_1 \wedge ... \wedge A_m \to B_n \}</math>.
Quando <math>n=1</math>, 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]].
FreqüentemetneFreqüentemente, é suficiente gerar uma FNC [[Satisfazibilidade|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==
::::<math>\forall x \exists z \exists y (\lnot P(x,z) \lor P(y,x)) </math>
Substituindo <math>[z := af(x), y := b, x_1 := c, x_2 := dg(x)]</math> :▼
::::<math>\forall x (\lnot P(x),f(x)) \lor P(g(x),x)) </math>
Passo 4) A fórmula já está na forma norma conjuntiva.
Passo 5) Colocar na "forma implicativa"de cláusulas:
::::<math>\{\lnot P(x),f(x)) \rightarrowlor P(g(x),x)\}</math>
Passo 6) Colocar em forma de cláusulas:
'''Exemplo 2''':::: <math>\{forall x ( \lnot \forall y (P(x,fy) \land \forall z \lnot R(xy,z)) \rightarrowland p(g\forall y \lnot P(x),xy)\}) </math>
'''Exemplo 2''': <math>\lnot \forall x (P(x,z) \land R(x,y)) \lor (\exists x P(x,z) \lor \forall x R(x,y)) </math> ▼
Passo 1) Colocar a fórmula na forma normal da negação:
::::<math>\existsforall x ( \lnot \forall y (P(x,zy) \land R(x,y)) \lorforall z (\existslnot x PR(xy,z)) \lorland \forall xy R\lnot P(x,y)) </math>
::::<math>\existsforall x (\lnotexists P(x,z) \lory \lnot R(P(x,y)) \lorland (\existsforall xz P\lnot R(xy,z)) \lorland \forall xy R\lnot P(x,y)) </math>
::::<math>\forall x_3 x( \exists y (\lnot P( cx, ay) \lor \lnot \forall z \lnot R( cy, bz)) \ lorland (P(d,a)\forall y \ lorlnot RP( x_3x, by)) ) </math> ▼▲'''Exemplo 2''': :::<math> \lnot \forall x (\exists y ( P(x,z) \ landlnot RP(x,y )) \lor (\exists xz PR( xy,z )) \ lorland \forall xy \lnot RP(x,y)) </math>
Passo 2) Skolemizar a fórmula:
::::<math>\forall x \exists x_1y_1 \exists x_2z \forall x_3y_2 (( \lnot P(x_1x,zy_1) \lor \lnot R(x_1y_1,yz)) \lor (P(x_2,z)land \lorlnot RP(x_3x,yy_2))) </math>
Substituindo <math>[y_1 := f(x), z := g(x)]</math>
::::<math>\exists z \exists y \exists x_1 \exists x_2 \forall x_3 (( \lnot P(x_1,z) \lor \lnot R(x_1,y)) \lor (P(x_2,z) \lor R(x_3,y))) </math>
▲Substituindo <math>[z := a, y := b, x_1 := c, x_2 := d]</math>:
▲::::<math>\forall x_3 ((\lnot P(c,a) \lor \lnot R(c,b)) \lor (P(d,a) \lor R(x_3,b))) </math>
Passo 3) Remover o quantificador universal <math>\forall x_3</math>: ▼
::::<math>((\lnot P(c,a) \lor \lnot R(c,b)) \lor (P(d,a) \lor R(x_3,b))) </math> ▼
::::<math>\ lnotforall P(c,a)x \ lorforall y_2 ((\lnot RP( cx, bf(x)) \lor R( Pf( dx), ag(x)) \ lorland R\lnot P( x_3x, by_2)) </math> ▼Passo 4) Colocar na forma normal conjuntiva: ▼
▲Passo 3) Remover oos quantificadorquantificadores universaluniversais <math>\forall x_3x</math> e <math>\forall y_2</math>:
▲::::<math>\lnot P(c,a) \lor \lnot R(c,b)) \lor (P(d,a) \lor R(x_3,b) </math>
▲::::<math>((\lnot P( cx, af(x)) \lor \lnot R( cf(x), bg(x)) \ lor (P(d,a)land \ lorlnot RP( x_3x, by_2)) ) </math>
Passo 5) Colocar na "forma implicativa":
▲Passo 4) ColocarA fórmula já está na forma normal conjuntiva :.
::::<math>(P(c,a) \land R(c,b)) \rightarrow (P(d,a) \lor R(x_3,b)) </math>
Passo 65) DistribuirColocar a implicação e colocar emna forma de cláusulas:
::::<math>\{(P(c,a) \landlnot RP(cx,bf(x)) \rightarrowlor PR(d,af(x), g(P(c,ax)) \land R(c,b)) \rightarrowlnot RP(x_3x,by_2)\}</math>
==Referências==
*[[Cláusula (lógica)]]
*[[Cláusula de Horn]]
*[[Forma normal prenex]]
*[[Lógica]]
|
