Lógica para Computação (IF61B)
Lógica para Computação
Prof. Celso Antônio Alves Kaestner, Dr. [email protected]
Lógica para Computação (IF61B)
20/04/23 Prof. Celso A A Kaestner 2
Algoritmo de Wang
• É um algoritmo que permite verificar a validade de um seqüente do tipo
B1, B2 … Bn |- A1, A2 … Am
• Equivale ao teorema
(B1 B2 … Bn ) ( A1 A2 … Am )
• O seqüente é representado por
(B1, B2 … Bn ) |-w (A1, A2 … Am)
Lógica para Computação (IF61B)
20/04/23 Prof. Celso A A Kaestner 3
Algoritmo de Wang
São aplicadas sucessivamente as regras:
1. (…,X,…)|-w(…) torna-se (…)|-w(…,X,…) e (…)|-
w(…,X,…) torna-se (…,X,…)|-w(…);
2. (…,XY,…)|-w(…) torna-se (…,X,Y,…)|-w(…) e (…)|-w(…,XY,…) torna-se (…)|-w(…,X,Y,…);
3. (…,XY,…)|-w(…) torna-se (…,X,…)|-w(…) e
(…,Y,…)|-w(…);
4. (…) |-w(…,XY,…) torna-se (…)|-w(…,X,…) e (…)|-w(…,Y,…);
Lógica para Computação (IF61B)
20/04/23 Prof. Celso A A Kaestner 4
Algoritmo de Wang
5. (…)|-w(…,XY,…) torna-se
(…)|-w(…,XY,…) e (…,XY,…) |-w(…) torna-se
(… XY,…) |-w (…);
6. (…,XY,…)|-w(…) torna-se
(…,(XY)(YX),…)|-w(…)
e (…)|-w(…,XY,…) torna-se
(…)|-w(…,(XY)(YX),…);
7. (…,X,…)|-w (…,X,…) torna-se T (true).
Lógica para Computação (IF61B)
20/04/23 Prof. Celso A A Kaestner 5
Algoritmo de Wang1. (p q), (q r), r |-w p
2. (p q),(q r), r |-w p (R5 x 2)
3. (p q),(q r) |-w p,r (R1)
4. p, (q r) |-w p, r q,(q r) |-w p,r (R3)
5. X q, q |-w p,r q, r |-w p,r (R3)
6. (R7) q |-w p,r, q X (R3)
7. X (R7)
(R7)
Lógica para Computação (IF61B)
20/04/23 Prof. Celso A A Kaestner 6
Algoritmo de Wang
• Prática do uso do algoritmo de Wang utilizando o software em Lisp.
Lógica para Computação (IF61B)
Formas Normais• Forma normal conjuntiva (fnc):
– Literal: variável proposicional ou sua negação;
– Cláusula: disjunção de literais;– Uma fbf está na fnc se é uma conjunção de
cláusulas;– Dada uma fbf A sempre é possível se
encontrar outra fbf B na fnc tal que A ≡ B.
20/04/23 Prof. Celso A A Kaestner 7
Lógica para Computação (IF61B)
Formas Normais• Obtenção da fnc:
1. Redefinir ↔ em função de →:
(A ↔B) ≡ (A →B) (B →A)
2. Redefinir → em função de e :
(A → B) ≡ ( A B)
3. Colocar os “para dentro”, de forma a obter os literais, usando as leis de De Morgan:
(AB ) (AB ) e (AB ) (A B)
20/04/23 Prof. Celso A A Kaestner 8
Lógica para Computação (IF61B)
Formas Normais4. Redistribuir os conectivos e usando a
distributividade, associatividade e comutatividade destes conectivos:
A (B C) (A B)(A C),
A (B C) ( A B) (A C),
A (B C) ( A B) C,
A (B C) ( A B) C,
A B B A, A B B A.
20/04/23 Prof. Celso A A Kaestner 9
Lógica para Computação (IF61B)
Formas NormaisExemplo:
p → (q (r p)) p (q (r p))
p (q ( r p)) p (q r p) (p q ) (p r) ( p p) (p q ) (p r) p
20/04/23 Prof. Celso A A Kaestner 10
Lógica para Computação (IF61B)
Formas Normais• Forma normal disjuntiva (fnd):
– Similar e dual à fnc;– Disjunção de conjunções de literais;– Obtenção similar à fnc, mudando apenas no
último passo quando da ordenação dos conectivos e .
20/04/23 Prof. Celso A A Kaestner 11
Lógica para Computação (IF61B)
Resolução• Cláusulas de Horn:
– Contém no máximo um literal positivo;– Podem ser de três tipos:
1. Regras: p1p2...pnq, equivalendo a (p1p2...pn) →q;
2. Fatos: cláusulas unitárias com um único literal positivo: p, q ...
3. Restrições: só contém literais negativos: p1p2...pn .
20/04/23 Prof. Celso A A Kaestner 12
Lógica para Computação (IF61B)
Resolução• É uma regra de inferência correta;
• Obtém uma cláusula resolvente a partir de duas cláusulas dadas, desde que estas tenham literais complementares:
A p B p A B
20/04/23 Prof. Celso A A Kaestner 13
Lógica para Computação (IF61B)
Resolução e refutação• O método dedutivo que usa a regra de
inferência resolução emprega refutação;
• Refutação: para provar |- A mostra-se que { A } |- (contradição).
20/04/23 Prof. Celso A A Kaestner 14
Lógica para Computação (IF61B)
Resolução e refutaçãoExemplo:
(p s r), (s r) |- p r
(p s r),(sr), (p r) |- (?) 1:(p s r), 2:(sr), 3:p , 4:r (de 1 e 3)
2:(sr), 4:r , 5:(s r) (de 4 e 5)
2:(sr), 4:r , 6: s (de 2 e 6)
4:r , 7: r (de 7 e 4) QED.
20/04/23 Prof. Celso A A Kaestner 15
Lógica para Computação (IF61B)
Resolução e refutação
• A linguagem PROLOG se fundamenta no princípio de resolução e em refutação, e será estudada mais adiante.
• Prática do uso do algoritmo de resolução / refutação utilizando o software em Lisp.
20/04/23 Prof. Celso A A Kaestner 16