Lógica para Computação

Lógica para Computação (IF61B)

Lógica para Computação

Prof. Celso Antônio Alves Kaestner, Dr. [email protected]


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)



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,…);



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).



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)



Algoritmo de Wang

• Prática do uso do algoritmo de Wang utilizando o software em Lisp.


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.



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)



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.



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



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 .



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 .



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



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).



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.



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.


Documents

Lógica para Computação