Lógica
Proposicional
Resolução
Notação na forma de
conjuntos




H=(PvQvR)^(PvQ)^(PvP)
Representação na forma de conjuntos:
H={[P,Q,R],[P,Q],[P]}
Note que


(PvQvR) = [P,Q,R]
(PvP)=[P]

Não é necessário representar duplicidade na
forma de conjuntos
Cláusulas e literais
complementares

Cláusula em lógica proposicional é uma
disjunção de literais



Usando a notação de conjuntos:
C1={P,Q,R}, C2={P,Q}, C3={P}
Dois literais são complementares
quando um é a negação do outro
Resolvente de 2 cláusulas

Supondo 2 cláusulas C1={A1,..., An} e
C2={B1, ..., Bn}, com literais
complementares





A, um conjunto de literais em C1, tal que
-A, um conjunto de literais complementares
a A, estão em C2
Resolvente de C1 e C2:
Res(C1,C2)=(C1-A)U(C2- -A)
Res(C1,C2) pode ser {}

Resolvente vazio ou trivial
Exemplo de resolvente




C1={P,Q,R} e C2={P,R}
Res (C1,C2) = {Q,R}, que também é
uma cláusula
D1={P,Q} e D2={P,Q}
Res (D1,D2) = {}, que também é uma
cláusula
Regra de Resolução

Supondo 2 cláusulas C1={A1,..., An} e
C2={B1, ..., Bn}, a Regra de Resolução
aplicada a C1 e C2 é:


Deduzir Res(C1,C2)
Para verificar satisfabilidade


Empregar várias vezes até obter a cláusula
vazia
Expansão por resolução
Expansão por resolução








{[P,Q,R],[P,R],[P,R]}
1. [P,Q,R]
2. [P,R]
3. [P,R]
4. [Q,R]
Res (1,2)
5. [Q,P]
Res (3,4)
6. [P]
Res (2,3)
(Não conseguimos obter a cláusula
vazia...)
Exemplo de expansão por
resolução










{[P,Q],[P,R],[P,Q],[Q,R]}
1. [P,Q]
2. [P,R]
3. [P,Q]
4. [Q,R]
5. [Q,R]
Res (1,2)
6. [P,R]
Res (3,5)
7. [Q,R]
Res (1,6)
8. {}
Res(4,7)
Expansão fechada – contém a cláusula vazia
Forma clausal

Dada uma fórmula H, a forma clausal
associada a H é


Uma fórmula Hc, uma conjunção de
cláusulas equivalente a H
Toda fórmula proposicional possui uma
forma clausal associada
Exercício




Achar a a forma clausal associada a:
(H^(GvH)) (H^G)v(H^H)
(H  G) (H  G)
((H))  H
Principais Leis

1 -Leis de eliminação



2 -Lei da negação


(H)  H
2 -Leis de De Morgan



PQ = (PvQ)
P  Q = (P  Q)^(Q  P)
(PvQ) = P ^ Q
(P^Q) = P v Q
3 -Leis distributivas:


F v (G^H) = (FvG) ^ (FvH)
F ^ (GvH) = (F^G) v (F^H)
Prova por resolução



Dadas uma fórmula H e Hc (forma
clausal associada a H)
Uma Prova de H por resolução é uma
expansão fechada sobre Hc
H é um teorema do sistema de
resolução
Exemplo de Prova por
resolução







H=((P1vP2vP3)^(P1P4)^(P2P4)^ (P3P4))
 P4
Determinar Hc associada a H
Hc=(((P1vP2vP3)^(P1P4)^(P2P4)^
(P3P4)) P4))
=(((P1vP2vP3)^(P1P4)^(P2P4)^(P3P4))
vP4)
=(P1vP2vP3)^(P1vP4)^(P2vP4)^(P3vP4)^
P4
={[P1,P2,P3],[P1,P4],[P2,P4],[P3,P4],[P4]}
Agora, é só fazer a expansão por resolução!
Exemplo de Prova por
resolução (cont.)









1.
2.
3.
4.
5.
6.
7.
8.
9.
[P1,P2,P3]
[P1,P4]
[P2,P4]
[P3,P4]
[P4]
[P2,P3,P4]
[P3,P4]
[P4]
{}
Res(1,2)
Res(3,6)
Res(4,7)
Res(5,8)
Exercício



H=((P1vP2)^(P1P4)^(P2P4)^
(P3P4))  P3
Determinar Hc associada a H
Fazer a expansão por resolução

Aberta ou fechada?
Conseqüência lógica na
resolução




Dada uma fórmula H e
um conjunto de hipóteses
b={H1,H2,...Hn},
então H é conseqüência lógica de b por
resolução
se existe uma prova por resolução de

(H1^H2^...^Hn)  H
Notação de Conseqüência
Lógica por Resolução

Dada uma fórmula H, se H é
conseqüência lógica de um conjunto de
hipóteses b={H1,H2,...Hn} por
resolução, diz-se que:
 b├ H ou
 {H1,H2,...Hn}├ H
Exercício de Conseqüência
Lógica por Resolução






Guga é determinado
Guga é inteligente
Se Guga é determinado, ele não é um
perdedor
Guga é um atleta se é amante do tênis
Guga é amante do tênis se é inteligente
“Guga não é um perdedor” é conseqüência
lógica das afirmações acima??
Solução



Provar H=(D^I^((D^A)P)^(TA)^(IT))
P
Mostrando que H é absurdo
 H=(D^I^((D^A)P)^(TA)^(IT))
P gera uma expansão por resolução
fechada a partir da sua forma clausal?
Resolução e Tableaux
[Fitting 1990]


Métodos por negação
Implementáveis



Em tableaux, usam-se preferencialmente as
regras que não bifurcam



Resolução (Julia Robinson 1965)
Prolog [Colmerauer 1972]
Bom para DNF
Em resolução, usamos CNF
Uma expansão fechada por resolução equivale
a um tableau fechado
Conjunto insatisfatível



Como provar que um conjunto de
fórmulas é insatisfatível?
Por exemplo:
b={AvB, (BvC), CD, (AvD)}
Conjunto insatisfatível (cont.)

b é insatisfatível sse
H= ((AvB)^(BvC)^(CD)^(AvD) for uma
tautologia
H é tautologia D Expansão por resolução associada a
Hc é fechada
Hc = (AvB)^B^C^(CvD)^A^D
Hc = {[A,B],[B],[C],[C,D],[A],[D]}

Portanto para provar que b é insatisfatível





Provar que ((AvB)^(BvC)^(CD)^(AvD)) é
tautologia
Conjunto insatisfatível (cont.)

b ={AvB, (BvC), CD, (AvD)} é
insatisfatível?


Provar que
((AvB)^(BvC)^(CD)^(AvD)) é
tautologia
Vimos na parte de semântica (Validade e
factibilidade)


H é válida D H é contraditória
Por resolução

Gerar uma expansão por resolução fechada para
(((AvB)^(BvC)^(CD)^(AvD)))
Conclusões

Dada uma fórmula da lógica proposicional H



H é tautologia D Expansão por resolução associada
a Hc (forma clausal de H) é fechada
H é contraditória (insatisfatível) DH é tautologia
D Expansão por resolução associada a Hc (forma
clausal de H) é fechada
H é refutável D Expansão por resolução associada
a Hc (forma clausal de H) é aberta
Exercício

Hoje é Sábado ou Domingo. Se hoje é
Sábado então é um fim de semana. Se
hoje é Domingo então é um fim de
semana. Portanto, hoje é um fim de
semana.
Exercício

Se hoje é Quinta-feira, então amanhã
será sexta-feira. Se amanhã for sextafeira, então depois de amanhã será
sábado. Conseqüentemente, se hoje for
quinta-feira, então depois de amanhã
será sábado.