Baixe o app para aproveitar ainda mais
Esta é uma pré-visualização de arquivo. Entre para ver o arquivo original
Clique para editar o estilo do título mestre Clique para editar o estilo do subtítulo mestre * * * Lógica Proposicional Resolução * * * Notação na forma de conjuntos H=(PvQvR)^(PvQ)^(PvP) Representação na forma de conjuntos: H={[P,Q,R],[P,Q],[P]} Note que (PvQvR) = [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)^(P1P4)^(P2P4)^ (P3P4)) P4 Determinar Hc associada a H Hc=(((P1vP2vP3)^(P1P4)^(P2P4)^ (P3P4)) P4)) =(((P1vP2vP3)^(P1P4)^(P2P4)^(P3P4))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)^(P1P4)^(P2P4)^ (P3P4)) 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)^(Q1R)^(QQ1)) P1 Mostrando que H é absurdo (P^Q^((P^R)P1)^(Q1R)^(QQ1)) 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] 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, (BvC), CD, (AvD)} * * * Conjunto insatisfatível (cont.) b é insatisfatível sse H= ((AvB)^(BvC)^(CD)^(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)^(BvC)^(CD)^(AvD)) é tautologia * * * Conjunto insatisfatível (cont.) b ={AvB, (BvC), CD, (AvD)} é insatisfatível? Provar que ((AvB)^(BvC)^(CD)^(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)^(BvC)^(CD)^(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) DH é 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ícios de Formalizaçã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, 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, SA, CS} |-- 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 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.
Compartilhar