Lógica de Predicados

Implementação de Resolução

Em Lógica de 1ª. Ordem Resolução não é uma simples extensão

da Resolução da Lógica Proposicional O processo é mais longo e cuidadoso:

Transformar a(s) fórmula(s) para a forma normal Prenex

Skolemizá-la(s) Transformá-las para CNF Transformá-las para a forma clausal Unificá-las durante a resolução

Por outro lado, ao usar a unificação, a resolução torna-se bem mais rápida do que os métodos de Gilmore e Davis-Putnam!

Resolução eficiente Idealmente todas as expansões

possíveis devem ser efetuadas Mas isso é caro computacionalmente!

Então organizemos os passos destas expansões num algoritmo e escolhamos melhor as expansões Devemos evitar gerar o que já existe, para

torná-lo eficiente Tentar ir o mais rápido possível para {}

Exemplo {[P],[P,Q],[Q, R],[R]} 1. [P]2. [P,Q]3. [Q, R]4. [R]5. [Q] 1,26. [P, R] 2,37. [Q] 3,48. [R] 3,59. [R] 1,610. [P] 4,611. [P] 2,712. {} 5,7

{[P],[P,Q],[Q, R],[R]}

1. [P]2. [P,Q]3. [Q, R]4. [R]5. [Q] 1,26. [Q] 3,47. {} 5,6

Rastro da resolução

[P] [P,Q] [Q, R] [R]

[Q] [P, R] [Q]

[R] [R] {} [P] [P]

Usos da resolução - decisões Exemplo genitor(X,Y) :- pai(X,Y). pai(adam,bill). pai(bill,carl). Para provar que adam é genitor de bill {[genitor(X,Y),pai(X,Y)],[pai(adam,bill)],

[pai(bill,carl)], [genitor(adam,bill)]}

Usos da resolução - decisões

1. [genitor(X,Y),pai(X,Y)]2. [pai(adam,bill)]3. [pai(bill,carl)]4. [genitor(adam,bill)]5. [genitor(adam,bill)] 1,26. [genitor(bill,carl)] 1,37. [pai(adam,bill)] 1,48. {} 4,59. {} 2,7

Usos da resolução - perguntas

Ou Consultas Quem é o genitor de Bill?? genitor(X,bill). X??? Incluir a seguinte cláusula na Base

[genitor(X,bill), Resp(X)] Por quê???

Usos da resolução - consultas1. [genitor(X,Y),pai(X,Y)]2. [pai(adam,bill)]3. [pai(bill,carl)]4. [genitor(X,bill),Resp(X)]5. [genitor(adam,bill)] 1,26. [genitor(bill,carl)] 1,37. [pai(X,bill),Resp(X)] 1,48. [Resp(adam)] 4,59. [Resp(adam)] 2,7

Pára quando achamos a(s) resposta(s)!

Sobre consultas

Pode resultar em mais de uma resposta

Se eu disser que mae(anne,bill) e pai (adam,bill) E perguntar “quem é genitor de bill?”

Usos da resolução - decisões1. [genitor(X,Y),pai(X,Y)]2. [genitor(X,Y),mae(X,Y)]3. [pai(adam,bill)]4. [mae(anne,bill)]5. [genitor(X,bill),Resp(X)]6. [genitor(adam,bill)] 1,37. [genitor(anne,bill)] 2,48. [pai(X,bill),Resp(X)] 1,59. [mae(X,bill),Resp(X)] 2,510. [Resp(adam)] 3,811. [Resp(anne)] 4,9

Consultas – informação incompleta Se eu disser que adam ou tom é pai

de bill e perguntar quem é pai de bill, o que acontecerá???

A resposta é adam ou tom:

1. [pai(adam,bill), pai(tom,bill)]2. [pai(X,bill),Resp(X)]3. [pai(tom,bill),Resp(adam)] 1,24. [Resp(adam),Resp(tom)] 2,3

Resolução eficiente na prática Escolher bem os resolventes a cada

passo (refinamentos) Diminuir o espaço de busca

(simplificação)

Todas as estratégias para melhorar o desempenho da resolução passam por atacar estes problemas

Estratégias de refinamento

Resolução Linear Construir uma linha, ao invés de uma

árvore de expansões Usar sempre a cláusula gerada por

último

Se pensarmos neste problema como uma busca para um caminho que contém a solução, que tipo de busca é essa??

Solução para “Cap. West”

Solução por resolução linear

Estratégias de refinamento

Estratégia Unitária Privilegiar cláusulas com um só literal Como pegamos cláusulas pequenas, há

garantia de chegarmos rápido a {} Porém, não é completa para qualquer

conjunto de cláusulas Mas é completa para cláusulas de Horn

A1 ^...An A

Estratégias de Simplificação

Eliminação de literais puros Um literal é puro se não existe no conjunto

de prova a sua negação Ex: {[P],[Q],[P,L],[L,Q],[P,Q,R], ,[R]}

L é puro, pois nunca será eliminado por resolução

Então é melhor retirar as cláusulas que o contém do processo de busca da {}

Se é para chegar a {}, podemos partir de {[P],[Q],[P,Q,R], ,[R]}

Estratégias de Simplificação

Descarte por englobamento (ou subsunção) Uma cláusula C1 engloba outra C2 sse existir

uma substituição O, tal que C1O C2 Se descartamos C2, não estamos perdendo a

insatisfatibilidade do conjunto, apenas apressando a chegada de {}

Ex1: P(x) P(y) v Q(z) Ex2: A v B v C, A v C, B v C

Resolvendo as 2 últimas, temos AvB, que engloba a 1ª.

Então o conjunto resultante seria A v B, A v C, B v C

Ajuda a resolução unitária

E este exemplo por linear?

{[P,Q],[P,Q],[P,Q],[P,Q]} Claramente insatisfatível!!

Porém IMPOSSÍVEL por linear (e tb por unitária) !!

Qual a vantagem das cláusulas de Horn para casos como este??

Resolução e Cláusulas de Horn É que sempre que aparece um

negado (o conseqüente), se ele existir em outra cláusula, ele não estará negado!

A1 ^...An A é {[A1],...[An],[A]} Então se existir prova, será fácil

encontrá-la Correto e completo e barato, se

existir prova

Exemplo em Prologavo(X,Y) :- genitor(X,Z), genitor(Z,Y).

^genitor(X,Y) :- pai(X,Y).genitor(X,Y) :- mae(X,Y).

pai(adam,bill).pai(bill,carl).mae(anne,bill).

Quem é avó(ô) nessa história????

?- true.Y=carl

?- gen(bill,Y).

X=adam

Árvore SLD?- avo(X,Y).

?- pai(bill,Y).?- m(bill,Y).

?- fail.

?- gen(X,Z),gen(Z,Y).

?- pai(X,Z),gen(Z,Y).

?- gen(carl,Y).

?- pai(carl,Y).?- m(carl,Y).

?- fail. ?- fail.

?- mae(X,Z),gen(Z,Y).

?- pai(bill,Y).?- mae(bill,Y).

?- true.Y=carl

?- fail.

?- pai(bill,Y).

X=anne

Conclusões

Paradigma de programação A ”função” membro, implementada como

relação: member(X,[X|Xs]). member(X,[Y|Ys]) :- member(X,Ys).

Vão-se gerando sentenças novas que precisam ser provadas até que uma é provada!

Pode entrar em loop, por falta do occur-check

Negação por falha em Prolog Prolog tem várias extensões (ex:LIFE,

CHR,...), com diferentes melhorias Prolog tem comandos built-in para

controlar a busca na árvore Ex: evitar insistir em determinados ramos

Operador de negação por falha em premissas: not p(X) verificado sse p(X) falha Isso é MUITO DIFERENTE de p(X) SER

FALSO, mas quebra o galho muitas vezes

Implementando resolução Prover boas estruturas de dados

Indexação e hashtables Boas ligações de pesquisa com BDs

BDs inteligentes ou dedutivos Estamos sempre recuperando literais para

tentar prová-los Bons algoritmos de unificação O problema reduz a busca em árvore

Obj: Reduzir o backtracking Ex: Residente(p,Itu)^Ocupacao(p,Presidente)