Upload
kipling
View
62
Download
0
Embed Size (px)
DESCRIPTION
Resolução. Aron Sebastian André Sousa Vivian Maria Márcio André . Resolução. P rincípio da Resolução A resolução na lógica de primeira ordem Exemplos. Princípio da Resolução. - PowerPoint PPT Presentation
Citation preview
Resolução
Aron SebastianAndré SousaVivian Maria
Márcio André
Resolução•Princípio da Resolução•A resolução na lógica de primeira ordem•Exemplos
Princípio da Resolução
O princípio da resolução é uma regra de inferência que dá origem a uma técnica de demonstração por refutação para sentenças e inferências da lógica proposicional e da lógica de primeira ordem.
A Resolução na Lógica de Primeira Ordem
A resolução na Lógica de primeira ordem condensa os silogismos tradicionais de inferência lógica em uma única regra. Para entender como a resolução funciona, considere o seguinte exemplo de silogismo da lógica aristotélica:Todos os gregos são
europeus.Homero é grego.Então, Homero é europeu.Ou de maneira mais geral: X.(P(X) implica Q(X)).P(a).Então, Q(a).
A Resolução na Lógica de Primeira Ordem
Para traçar o raciocínio usado na técnica de resolução, primeiro as cláusulas devem ser convertidas para a forma normal conjuntiva. Nessa forma, todas as quantificações se tornam implícitas: quantificadores universais em variáveis (X, Y...) são simplesmente omitidos quando subentendidos, enquanto variáveis em quantificadores existenciais são substituídas por funções de Skolem.¬P(X) V Q(X)
P(a) Então, Q(a)
A Resolução na Lógica de Primeira Ordem
Então a questão é, como a técnica de resolução deriva a ultima cláusula a partir das duas primeiras? A regra é simples:
•Encontre duas cláusulas contendo o mesmo predicado, onde uma cláusula é negada e a outra não.•Faça a unificação em ambos os predicados. (Se a unificação falhar, então você fez uma má escolha de predicados. Volte para o passo anterior e tente novamente.)
A Resolução na Lógica de Primeira Ordem
•Se, após a unificação, alguma variável não-ligada que foi ligada nos predicados unificados também ocorre em outros predicados nas duas cláusulas, então substitua pelos seus respectivos termos ligados.•Descarte os predicados unificados, e combine o restante das duas cláusulas em uma nova cláusula.
A Resolução na Lógica de Primeira Ordem
Para aplicar essa regra no exemplo acima, nós encontramos o predicado ‘P’ na forma negada na primeira cláusula:¬P(X)E em forma não negada na segunda cláusula: P(a)X é uma variável livre, enquanto a é um átomo. Unificando os dois obtemos a substituição: = [(a,X)]Descartando os predicados unificados, e aplicando a substituição dos predicados restantes (apenas Q(X), nesse caso), obtemos a conclusão: Q(a)
A Resolução na Lógica de Primeira Ordem
Para um outro exemplo, considere a forma silogística:Todos os políticos são corruptos.Todos os corruptos são mentirosos.Então todos os políticos são mentirosos.Ou de maneira mais geral:X P(X) implica Q(X)X Q(X) implica R(X)Então, X P(X) implica R(X)
A Resolução na Lógica de Primeira Ordem
Na FNC (Forma Normal Conjuntiva):¬P(X) V Q(X)¬Q(Y) V R(Y)
(Note que a variável na segunda cláusula foi renomeada pra deixar claro que variáveis em cláusulas diferentes são distintas)
Agora, unificando Q(X) na primeira cláusula com Q(Y) na segunda cláusula temos que X e Y se tornam a mesma variável. Efetuando esta substituição nas cláusulas restantes e combinando-as, temos a conclusão:¬P(X) V R(X)
Exemplos de Resolução
Toda pessoa é sábia ou tucana. Zé não é tucano. Zé é sábio? U=pessoas I[q(x)]=T sse x é sábio I[p(x)]=T sse x é tucana I[a]=Zé
Exemplos de ResoluçãoCont. Toda pessoa é sábia ou tucana. Zé não é tucano. Zé é sábio? (x)(p(x)v q(x))^ p(a)q(a)
Exemplos de ResoluçãoCont. Por refutação: ((x)(p(x)v q(x))^ p(a)q(a)) (((x)(p(x)v q(x))^ p(a)) v q(a)) (x)(p(x)v q(x))^ p(a)) v q(a)) (x)(p(x)v q(x))^ p(a)) ^ q(a)) {[p(x),q(x)], [p(a)], [q(a)]}
Exemplos de ResoluçãoCont. Agora, é só fazer a expansão por
resolução! 1. [p(x),q(x)] 2. [p(a)] 3. [q(a)] 4. [q(a)] Res(1,2), O1={xa} 5. {} Res(3,4), O2={xa}
Exemplos de Resolução Tonha gosta de quem não se
valoriza. Não existe ninguém que se
valorize e que Tonha goste?
Exemplos de Resolução Cont. v(x) = x se valoriza g(x,y) = x gosta de y a = Tonha (Antônia)
Exemplos de Resolução Cont.
(x)(v(x)^g(a,x))(y)(v(y)^g(a,y))(x)(v(x)^g(a,x))(y)(v(y)^g(a,y))((x)(v(x)^g(a,x)) v (y)
(v(y)^g(a,y)))(x)(v(x)^g(a,x)) ^ (y)(v(y)^g(a,y)))
Conclusões Dada uma fórmula da lógica de
predicados H H é tautologia D EXISTE uma Expansão por
resolução associada a Hc (forma clausal de H) que é fechada
H é contraditória (insatisfatível) DH é tautologia D EXSTE uma Expansão por resolução associada a Hc (forma clausal de H) que é fechada
H é refutável D TODA Expansão por resolução associada a Hc (forma clausal de H) é aberta