Lógica de Predicados Implementação de Resolução. Em Lógica de 1ª. Ordem Resolução não é...

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 conjuntiva

Skolemizá-la(s) 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 competitiva em relação ao DPLL otimizado (Chaff)!

Algoritmos para gerar CNF (repetidamente)

1 -Leis de eliminação P Q = (P Q)^(Q P) PQ = (PvQ)

2 -Leis da negação (H) H ((z)(H)) = ((x)H),((z)(H)) = ((x)H)

2 -Leis de De Morgan (PvQ) = P ^Q, (P^Q) = P v Q

3 – Renomeação de variáveis 4 – Distributiva: F v (G^H) = (FvG) ^ (FvH)

Exemplo 1 de Skolemização

(x)arma(x) Então posso transformar isso em

arma(M1) Desde que M1 ainda não exista na prova

ou na base de conhecimento!

Exemplo 2 de Skolemização

(x)(y)prof(y,x) todo aluno tem ao menos um professor

Se trocarmos para (x)(Fred,x) Fred é professor de todos os alunos do CIn Não é uma interpretação correta do predicado

Porque acontece isso??

Função de Skolem

Porque Fred existe no domínio A idéia é que b seja “um professor

genérico” de x (sem ser uma variável ) y=f(x), pois y depende de x

Trocamos (x)(y)r(y,x) para (x)r(f(x),x) (z)(x)(y)p(z,y,x) vira (z)

(x)p(z,g(z,x),x)

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

Importância da igualdade

É importante dotar nossa linguagem de igualdade Equals(a,b) ou a=b Se concluirmos P(a), então tb

concluímos P(b) Q(a,b) pode ser resolvida com ¬Q(b,a) ...

Propriedades da igualdade Reflexividade: (x) x=x Simetria: (x,y) x=y y=x Transitividade: (x,y,z)

(x=y)^(y=z)(x=z) Mesmo assim, ainda não podemos

provar que P(b) a partir de P(a)... Só se pudermos substituir termos iguais Porém, custo caro computacionalmente

Tratamento da igualdade Paramodulação:regra de inferência

a ser usada junto com a regra de resolução

Se temos as cláusulas m1 = [Px(t)] U m’1, onde t é um

termo M2 = (a=b) U m’2 O é um unificador entre t e a

Então o paramodulante binário é PM=PxO(bO) U m’1O U m’2O

Exemplo de paramodulação ¬P(x) v Q(h(x))

Px(t)= Q(h(x)), t=h(x) e m’1=¬P(x) ¬R(y) v (h(y) = g(y,f(y))

a = h(y), b=g(y(,f(y)) e m’2= ¬R(y) t e a (h(x) e h(y)) têm um unificador

O = {xy}

PM=PO(bO) U m’1O U m’2O PM= Q(g(y,f(y))) v ¬P(y) v ¬R(y)

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

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 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??

Problema de Prova

Law: it is crime for an American to sell weapons to hostile nations. Country Nono, an enemy of USA, has some missiles, sold by American Cel. West.

Como fazer um sistema provar que West é criminoso??

Sentenças especificadas em lógica de 1a. ordem

Lei: x,y,z American(x)^Weapon(y)^Nation(z)^Hostile(z)^

Sells(x,y,z)=> Criminal(x) Inimigo é hostil:x Enemy(x,America) => Hostile(x) Mísseis são armas: x Missile(x) => Weapon(x) Nono e USA são países inimigos

Country(Nono), Country(America), Enemy(Nono,America)

West é americano: American(West) Nono tem mísseis... x Owns(Nono,x)^Missile(x) ...vendidos por West

x Owns(Nono,x)^Missile(x) =>Sells(West, Nono,x)

Prova

Solução para “Cap. West”

Solução por resolução linear

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??

Porque é bom usar cláusulas de Horn para realizar a resolução??

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 É fácil

SAT, Horn-SAT e conversões

Using a linear algorithm for unit propagation, the algorithm is linear in the size of the formula.

It is logical to wonder if Horn-SAT can be used to prove that P=NP, by converting any SAT problem to a Horn-SAT problem and then solving it in polynomial time.

Problems: Transforming a SAT problem to a Horn-SAT

problem takes exponential time. The resultant transformation is exponential in

length.

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

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

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

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

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)