Lógica de
Predicados
Estratégias de Resolução
Defeitos da resolução

Apesar de, para lógica de predicados,
resolução ser bem melhor que o
algoritmo de Gilmore


Mas ainda podemos melhorá-la!
Durante a resolução, em ambas as
lógicas, há

passos e cláusulas não usados na prova
Exemplo (proposicional)






Darcy
Darcy  Criança
Criança ^ Macho  Garoto
Infantil  Criança
Criança ^ Fêmea  Garota
Fêmea


Isto deriva
Garota????
Em Cláusulas



[Darcy]
[Darcy,Criança]
[Criança,Macho,Garoto]



[Infantil,Criança]
[Criança,Fêmea,Garota]



[(Criança ^ Macho), Garoto]
[(Criança ^ Fêmea),Garota]
[Fêmea]
[Garota] (conseqüência lógica)
Prova gráfica

[Darcy]
[Darcy,Criança]

[Criança]
[Criança,Fêmea,Garota]

[Fêmea,Garota] [Fêmea]

[Garota]

{}
[Garota]
Estratégias mais eficientes

Estratégias de Deleção (ou simplificação)




Tautologias
Subsunções
Literais puros
Estratégias de refinamento




Resolução de entrada
Resolução de unidade
Resolução linear
…
Estratégias de Deleção Tautologias

Tirar tautologias do conjunto de cláusulas






ANTES da unificação
Sua ausência não afeta a prova
Ex: {[P(a), P(a)], [P(a), Q(x), Q(y)]}
Depois da unificação
Ex: {[P(a), P(x)], [P(a)],[P(b)]}
Se retirarmos [P(a), P(x)], já que são
complementares se unificados????
Estratégias de Deleção Subsunções

C1 subsume C2 sse existe O tal que



C1O  C2O
Retirar C2 não altera a prova
Exs:



P(x) subsume P(y) v Q(z)
P(x) subsume P(a)
P(y) v Q(a) subsume P(f(a)) v Q(a) v R(y)
Estratégias de Deleção Literais puros


Um literal é puro sse se seu
complemento (unificável ou não) não
existir nas cláusulas
Ex: {[R, P, Q], [P, S], [Q, S], [P],
[Q], [R]}


S é puro
Cláusulas que o contém podem ser
deletadas pois não serão eliminadas na
resolução!
Estratégias de refinamento

Resolução de unidade

Procura-se empregar cláusulas unitárias



Eficiente mas incompleta, se o conjunto de
cláusulas não contiver unitárias o suficiente
Resolução de entrada




Com um só literal
Usar pelo menos uma cláusula do conjunto inicial
Equivalente à de unidade
Completo para cláusulas de Horn
Exemplo de falha de ambos

{[P, S], [P, S], [P, S], [P, S]}
Cláusulas de Horn





Do tipo A1^...^An  B, que vira
[A1,...,An, B]
Só há um literal positivo: o conseqüente
Lê-se: se A1 e ... e An então B
Bons para estruturar conhecimento e
controlar a inferência
Resolução SLD

Resolução Linear com função de
Seleção para cláusulas Definidas




Generalização de resolução de entrada
Sempre usam-se cláusulas do conjunto de
entrada ou suas filhas em 1º. grau
Boa para cláusulas de Horn
Busca-se tentar provar diretamente a
conseqüência lógica
O exemplo da garota
Garota
Criança
Fêmea
Darcy
No conjunto inicial tínhamos
Criança ^ Fêmea  Garota
([Criança,Fêmea,Garota])
Example [U. Nilsson]
gp(X,Y) :- p(X,Z), p(Z,Y).
p(X,Y) :- f(X,Y).
p(X,Y) :- m(X,Y).
f(adam,bill).
f(bill,carl).
m(anne,bill).
Queries


A query is an expression of the form:
?- A1, ..., An.
where n=0,1,2,... and A1, ..., An are
atomic formulas.
Examples:
?- father(X, bill).
?- parent(X, bill), male(X).
Interpretation Queries

Consider a query ?- A1, ... , An.

Declarative (logical) reading:
Are there values of the variables
such that A1 and...and An?

Procedural (operational) reading:
First solve A1, then A2 etc
Ground SLD-Resolution
?- A1,A2,...,An.
A1 :- B1,...,Bm.
?- B1,...,Bm,A2,...,An.
where
A1 :- B1,...,Bm is an instantiated program clause.
A Derivation
parent(X,Y) :father(X,Y).
parent(X,Y) :mother(X,Y).
father(adam,bill).
mother(anne,bill).
?- parent(adam,bill)
?- father(adam,bill)
?- true
Another Derivation
parent(X,Y) :father(X,Y).
parent(X,Y) :mother(X,Y).
father(adam,bill).
mother(anne,bill).
?- parent(anne,bill)
?- mother(anne,bill)
?- true
Full SLD-Resolution
?- A1,A2,...,An.
B0 :- B1,...,Bm.
?- (B
A1=
B0, mB,A
1,...,B
m,A
2,...,An.
1,...,B
2,...,A
n)q.
where:
• B0 :- B1,...,Bm is a renamed program clause.
• q is a solution to the equation A1 = B0.
Yet Another Derivation
?- parent(X,bill).
?- father(X,bill).
X=X1, bill=Y1, father(X1,Y1).
?- true.
X=adam, bill=bill.
parent(X1,Y1)
father(adam,bill).
Answer::-X=adam
father(X1,Y1).
And Another One...
?- gp(X,Y).
X=adam
?- p(X,Z1),
X=X1, Y=Y1,
p(Z1,Y).
p(X1,Z1), p(Z1,Y1).
Y=carl
?- f(X,Z1),
X=X2, Z1=Y2,
p(Z1,Y).
f(X2,Y2), p(Z1,Y).
?- X=adam,Z1=bill,
p(Z1,Y).
p(bill,Y).
?- f(bill,Y).
bill=X3, Y=Y3, f(X3,Y3).
?- bill=bill,
true.
Y=carl.
gp(X1,Y1)
p(X2,Y2)
p(X3,Y3)
f(adam,bill).
:f(bill,carl).
p(X1,Z1),p(Z1,Y1).
:- f(X3,Y3).
f(X2,Y2).
And a Failed One...
?- gp(X,Y).
X=bill
?- p(X,Z1),
X=X1, Y=Y1,
p(Z1,Y).
p(X1,Z1), p(Z1,Y1).
?- f(X,Z1),
X=X2, Z1=Y2,
p(Z1,Y).
f(X2,Y2), p(Z1,Y).
?- X=bill,Z1=carl,
p(Z1,Y).
p(carl,Y).
?- f(carl,Y).
carl=X3, Y=Y3, f(X3,Y3).
?- fail.
gp(X1,Y1)
p(X2,Y2)
p(X3,Y3)
FAILURE!!!
:f(bill,carl).
p(X1,Z1),p(Z1,Y1).
:- f(X3,Y3).
f(X2,Y2).
SLD-Tree
?- gp(X,Y).
?- p(X,Z),p(Z,Y).
X=adam
?- f(X,Z),p(Z,Y).
?- p(bill,Y).
X=anne
?- m(X,Z),p(Z,Y).
?- p(carl,Y).
?- p(bill,Y).
?- f(carl,Y). ?- m(carl,Y).
?- f(bill,Y).
?- f(bill,Y). ?- m(bill,Y).
?- true.
Y=carl
?- fail.
?- fail.
?-?-fail.
true.
Y=carl
?- m(bill,Y).
?- fail.
Logic Programming
•
SLD-resolution:


Soundness:
if qn… q2q1 is a computed answer, then P |= qn… q2q1G
Completeness:
if P |= qG, then there exists a computed answer s such
that q = s for some 
Example:
p(X,Z)  q(X,Y), p(Y,Z)
p(X,X)
q(a,b)
Logic Programming
•
PROLOG (Alain Colmerauer 1972):


Only Horn sentences are acceptable
The occur-check is omitted from the unification 
unsound
Example:

test  p(X,X)
p(X,f(X))
Backward chaining with depth-first search  incomplete
Example:
p(X,Y)  q(X,Y)
p(X,X)
q(X,Y)  q(Y,X)
Logic Programming
Infinite
SLD-tree:

p(X,b)
 q(X,b)
{X/b}
 q(b,X)
succes
s
 q(X,b)
Logic Programming
•
PROLOG (Alain Colmerauer 1972):

Unsafe cut  incomplete
Example:
A  B, C
B  D, !, E
D
A
 B, C
 D, !, E, C
 !, E, C

Negation as failure:  P if fails to prove P
Muito obg!




Gostei de trabalhar com vcs!!
Desculpem as escorregadas!
Estudem e boas provas!
E depois...
BOAS FÉRIAS!