Cap7 - Parte2 (Resolução)

Esta é uma pré-visualização de arquivo. Entre para ver o arquivo original

*
*
*
*
Capítulo 7
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
*
*
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...)
*
*
Construção de uma expansão por resolução (recursiva)
Supondo um conjunto de cláusulas 		{A1,..., An}
1. A1
...
n. An é uma expansão por resolução
Se Exp* resulta da adição de Res(Ai,Aj), i,j<=n, i diferente de j a uma expansão Exp
Exp* também é uma expansão por resolução sobre {A1,..., An}
*
*
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]		Res(1,2)
7. [P3,P4]		Res(3,6)
8. [P4]			Res(4,7)
9. {}			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 de refutação - por negação
Implementáveis 
Resolução (Julia Robinson 1965)
Prolog [Colmerauer 1972]
Em tableaux, usam-se preferencialmente as regras que não bifurcam
Bom para CNF
Em resolução, usamos DNF
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)}
*
*
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 sexta-feira, então depois de amanhã será sábado. Conseqüentemente, se hoje for quinta-feira, então depois de amanhã será sábado.