23 - Estratégias de Resolução

Esta é uma pré-visualização de arquivo. Entre para ver o arquivo original

Clique para editar o estilo do título mestre
Clique para editar o estilo do subtítulo mestre
*
*
*
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] 
[(Criança ^ Macho), Garoto]
[Infantil,Criança]
[Criança,Fêmea,Garota]
[(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
Com um só literal
Eficiente mas incompleta, se o conjunto de cláusulas não contiver unitárias o suficiente
Resolução de entrada
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.
 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)
parent(X,Y) :-
	father(X,Y).
parent(X,Y) :-
	mother(X,Y).
father(adam,bill).
mother(anne,bill).
parent(X,Y) :-
	father(X,Y).
parent(X,Y) :-
	mother(X,Y).
father(adam,bill).
mother(anne,bill).
*
*
*
Another Derivation
parent(X,Y) :-
	father(X,Y).
parent(X,Y) :-
	mother(X,Y).
father(adam,bill).
mother(anne,bill).
?- parent(anne,bill)
parent(X,Y) :-
	father(X,Y).
parent(X,Y) :-
	mother(X,Y).
father(adam,bill).
mother(anne,bill).
parent(X,Y) :-
	father(X,Y).
parent(X,Y) :-
	mother(X,Y).
father(adam,bill).
mother(anne,bill).
*
*
*
Full SLD-Resolution
?- A1,A2,...,An.
*
*
*
Yet Another Derivation
?- parent(X,bill).
parent(X1,Y1) :- father(X1,Y1).
father(adam,bill).
*
*
*
And Another One...
?- gp(X,Y).
gp(X1,Y1) :- p(X1,Z1),p(Z1,Y1).
p(X2,Y2) :- f(X2,Y2).
f(adam,bill).
p(X3,Y3) :- f(X3,Y3).
f(bill,carl).
*
*
*
And a Failed One...
?- gp(X,Y).
gp(X1,Y1) :- p(X1,Z1),p(Z1,Y1).
p(X2,Y2) :- f(X2,Y2).
f(bill,carl).
p(X3,Y3) :- f(X3,Y3).
FAILURE!!!
*
*
*
SLD-Tree
?- gp(X,Y).
*
*
*
Logic Programming
SLD-resolution:
Soundness: 
		if n… 21 is a computed answer, then P |= n… 21G
			
Completeness: 
		if P |= G, then there exists a computed answer s such 		that  = 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
 p(X,b)
 q(X,b)
{X/b}
success
 q(b,X)
 q(X,b)
Infinite SLD-tree:
*
*
*
Logic Programming
PROLOG (Alain Colmerauer 1972):
Unsafe cut  incomplete
	Example: 	A  B, C			  A
				B  D, !, E
				D 			  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!