Lógica
Proposicional
Formas Normais
e Resolução
Formas normais e {,v,^}



Um literal é um símbolo proposicional
ou sua negação
Um bom conjunto completo é {,v,^}
Formas normais são obtidas a partir
desse conjunto de conectivos
Forma normal disjuntiva


Uma fórmula está na forma normal
disjuntiva (fnd ou DNF, em inglês) se é
uma disjunção de conjunções de literais
F é da forma F1 v F2 v ... v Fn, onde



Fi é uma conjunção (da forma
A1 ^ A2 ^ ... ^ An ) e
Ai é um literal
Ex: H=(P^Q) v (R^Q^P) v (P^S)
Forma normal conjuntiva


Uma fórmula está na forma normal
conjuntiva (fnc ou CNF, em inglês) se é
uma conjunção de disjunções de literais
F é da forma F1 ^ F2 ^ ... ^ Fn, onde



Fi é uma disjunção (da forma
A1 v A2 v ... v An ) e
Ai é um literal
Ex: G=(PvQ) ^ (RvQvP) ^ (PvS)
Obtenção de formas normais

Observe que H e G são parecidos



H=(P^Q) v (R^Q^P) v (P^S), DNF
G=(PvQ) ^ (RvQ vP) ^ (PvS), CNF
Para obtê-las a partir de fórmulas
quaisquer usam-se algoritmos duais

Os mesmos, trocando-se T por F
Algoritmos usando leis
(repetidamente)

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)
Exercícios

Obter DNF de (P v Q) R




= (PvQ) v R (eliminação de )
= (P ^ (Q)) v R (De Morgan)
= (P ^ Q) v R (negação)
Obter CNF de (P^(QR))S
Exercícios de obtenção de
formas normais


Obter DNF de (P ^Q) R
Obter CNF de (P ^Q) R
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
Sistema com Resolução



Alfabeto da Lógica Proposicional
Conjunto de cláusulas da Lógica
Proposicional
A regra de resolução
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
Prova por resolução



Dadas uma fórmula H e Hc, a 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. [P1,P2,P3]
2. [P1,P4]
3. [P2,P4]
4. [P3,P4]
5. [P4]
6. [P2,P3,P4]
7. [P3,P4]
8. [P4]
9. {}
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=(P^Q^((P^R)P1)^(Q1R)^(QQ1))
P1
Mostrando que H é absurdo
(P^Q^((P^R)P1)^(Q1R)^(QQ1))
P1) gera uma expansão por resolução
fechada a partir da sua forma clausal?
Resolução e Tableaux

Quais as relações entre eles??
Resolução e Tableaux [Fitting
1990]


Métodos por negação
Implementáveis



Resolução [Julia Robinson 1965]
Prolog [Colmerauer 1972]
Uma expansão fechada por resolução
equivale a um tableau fechado
Resolução





Olha para o significado
da fórmula
Uma disjunção
mantém-se numa
cláusula
Uma conjunção
“bifurca” cláusulas
Linhas de resoluções
Pega-se uma conjunção
de disjunções e tenta-se
simplificá-la
x Tableaux



Olha para o valor da
fórmula
As regras disjuntivas
bifurcam tableaux
São usadas árvores

Representam
naturalmente disjunções
entre ramos
Em resolução...

Na CNF, para converter uma fórmula
para a forma clausal, os ‘v’s criam
cláusulas seqüenciais e os ‘^’s separam
os termos



Exs: AvB = {[A,B]}; A^B ={[A],[B]}
o que, na prática, vira uma bifurcação
Resolução ocorre sobre CNFs
Exercícios de Formalização

A proposta de auxílio está no correio.
Se os árbitros a receberem até sextafeira, eles a analisarão. Portanto, eles a
analisarão porque se a proposta estiver
no correio, eles a receberão até sextafeira. (C, S, A)
Solução

A proposta de auxílio está no correio. Se os
árbitros a receberem até sexta-feira, eles a
analisarão. Portanto, eles a analisarão porque
se a proposta estiver no correio, eles a
receberão até sexta-feira.
C: A proposta de auxílio está no correio.
S: Os árbitros recebem a proposta até Sexta-feira.
A: Os árbitros analisarão a proposta.
{C, SA, CS} |-- A
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.