Lista de linguagens

Prévia do material em texto

Resolução e unificação 
 
É denominado resolução o ato de se fazer uma única inclusão a partir de um par de 
cláusulas de Horn. 
 
Definição: quando aplicada às cláusulas de Horn, a resolução diz que se h é a cabeça de 
uma cláusula de horn e ela corresponde a um dos termos de uma outra cláusulas de horn, 
então aquele termo pode ser substituído por h. 
 
Em outras palavras, se nós temos as cláusulas: h<-terms 
t<-t1, h, t2 
 
então podemos resolver a segunda cláusula para t <- t1, termr, t2 por exemplo: 
 
fala(mary, Ingles)<- true 
fala_com(x,y)<-fala(X,L), fla(Y,L) x diferente de y 
 
Com a hipótese de que às variáveis X e L são atribuídas os valores “mary” e “Ingles” na 
segunda regra. A resolução, por tanto, ajuda a chegar às conclusões. 
Definição: a atribuição de valores a variáveis durante a resolução é chamada instanciação. 
Definição: unificação é um processo e correspondência de padrões que determina que 
instâncias, em particular, podem ser feitas a variáveis ao mesmo tempo em que se faz uma 
série de resoluções simultâneas. 
 
fala(allen, russo) 
fala(bob, Ingles) 
fala(mary, russo) 
fala(mary, Ingles) 
 
conversa_com(X, Y):- fala(X, Y), fala(Y,L), X\=Y. 
 
conversa_com(allen, bob) 
H={russo, Ingles, allen, bob, mary}