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

1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
12.
{[P],[P,Q],[Q, R],[R]}
[P]
[P,Q]
[Q, R]
[R]
[Q]
1,2
[P, R] 2,3
[Q]
3,4
[R]
3,5
[R]
1,6
[P]
4,6
[P]
2,7
{}
5,7

1.
2.
3.
4.
5.
6.
7.
{[P],[P,Q],[Q, R],[R]}
[P]
[P,Q]
[Q, R]
[R]
[Q]
1,2
[Q]
3,4
{}
5,6
Rastro da resolução
[P]
[P,Q]
[Q]
[R]
[Q, R]
[P, R]
[R]
{}
[R]
[Q]
[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.
2.
3.
4.
5.
6.
7.
8.
9.
[genitor(X,Y),pai(X,Y)]
[pai(adam,bill)]
[pai(bill,carl)]
[genitor(adam,bill)]
[genitor(adam,bill)]
[genitor(bill,carl)]
[pai(adam,bill)]
{}
{}
1,2
1,3
1,4
4,5
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 - consultas
1.
2.
3.
4.
5.
6.
7.
8.
9.
[genitor(X,Y),pai(X,Y)]
[pai(adam,bill)]
[pai(bill,carl)]
[genitor(X,bill),Resp(X)]
[genitor(adam,bill)]
1,2
[genitor(bill,carl)]
1,3
[pai(X,bill),Resp(X)]
1,4
[Resp(adam)]
4,5
[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ões
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
[genitor(X,Y),pai(X,Y)]
[genitor(X,Y),mae(X,Y)]
[pai(adam,bill)]
[mae(anne,bill)]
[genitor(X,bill),Resp(X)]
[genitor(adam,bill)]
1,3
[genitor(anne,bill)]
2,4
[pai(X,bill),Resp(X)]
1,5
[mae(X,bill),Resp(X)] 2,5
[Resp(adam)]
3,8
[Resp(anne)]
4,9
Consultas – informação
incompleta


1.
2.
3.
4.
Se eu disser que adam ou tom é pai de bill
e perguntar quem é pai de bill, o que
acontecerá???
A resposta é adam ou tom:
[pai(adam,bill), pai(tom,bill)]
[pai(X,bill),Resp(X)]
[pai(tom,bill),Resp(adam)]
1,2
[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 Prolog
avo(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????
Árvore SLD
?- avo(X,Y).
?- gen(X,Z),gen(Z,Y).
X=adam
?- pai(X,Z),gen(Z,Y).
?- gen(bill,Y).
X=anne
?- mae(X,Z),gen(Z,Y).
?- gen(carl,Y).
?- pai(bill,Y).
?- pai(carl,Y).?- ?m(carl,Y).
pai(bill,Y). ?- mae(bill,Y).
?- pai(bill,Y). ?- m(bill,Y).
?- true.
Y=carl
?- fail.
?- fail.
?-?-fail.
true.
Y=carl
?- fail.
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


Boas ligações de pesquisa com BDs




Indexação e hashtables
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)