Aplicação e Composição de Substituições
A resolução com cláusulas que contêm variáveis é similar à
resolução proposicional mas requer a aplicação de
substituições com o intuito de substituir certas variáveis por
termos específicos.
Seja a substituição  = {X1/t1, X2/t2,..., Xn/tn}
Como já vimos, uma aplicação de  numa fórmula W é a
substituição de todas as ocorrências livres da variável Xi pelo
termo ti.
O resultado é chamado de instância da substituição e é
denotado por W.
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
186
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Aplicação e Composição de Substituições
Considere-se a fórmula
W = gosta(X, Y)
se aplicarmos a W a substituição 1 = {X/ana, Y/luis} temos a
instância da substituição
W1= gosta(ana, luis).
se aplicarmos a W a substituição 2 = {X/Y, Y/luis} temos a
instância da substituição
W2= gosta(Y, luis)
e aplicando uma vez mais 2 ficamos com
(W2)2 = gosta(luis, luis).
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
187
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Aplicação e Composição de Substituições
Nem todas as substituições são válidas.
Para que o sejam devem respeitar as seguintes propriedades:
Funcionalidade: {U1/t1, ..., Um/tm} todas as variáveis Ui devem
ser distintas.
Por exemplo {X/ana, Y/luis, Y/miguel} não é uma substituição
válida porque não respeita a propriedade acima.
Idempotência: para qualquer fórmula W deve ter-se que
W = (W)
ou seja, o resultado de aplicar a substituição uma vez deve ser
igual ao resultado de aplicá-la n vezes (com n>1)
Assim a substituição 2 não é considerada válida.
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
188
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Aplicação e Composição de Substituições
A operação mais importante entre substituições é a composição.
Suponhamos que temos duas substituições válidas:
1 = {U1/t1, ..., Um/tm}
2 = {V1/s1, ..., Vn/sn}
a composição de 1 com 2 é denotada pela expressão 1  2 e é
definida como
{U1/t12, ..., Um/tm2}  {Vj/sj | Vj  {U1, ..., Um}}
ou seja, aplicar 1 a W representa substituir todas as suas variáveis
livres Ui pelos termos ti resultando na instância W1. Depois restam
apenas duas formas da substituição 2 alterar W1:
substituir todas as variáveis Vj introduzidas por 1
substituir todas as variáveis Vj que não foram substituídas por 1
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
189
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Aplicação e Composição de Substituições
Nem todas as composições são completamente válidas uma vez que
nem todas respeitam a propriedade da idempotência. No entanto
possuem todas as seguintes propriedades:
1  2 é funcional
W(1  2 ) = (W 1)2
(1  2)  3 = 1  (2  3)
para qq fórmula W
associatividade de 
Mas a composição não é, em geral, comutativa.
Prove que a composição não é comutativa utilizando a fórmula
W = p(U1, g(V1), V2)
e as substituições
1 = {U1/ f(V1)}
2 = {V1/a, V2/b, U1/c}
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
190
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Resolução em Lógica de Predicados
De forma a utilizarmos a resolução para as cláusulas da lógica de
predicados teremos de suplementar essa regra de inferência com
o uso implícito de outra regra conhecida como instanciação
universal:
(X)W(X)├ (Y1) ... (Yn)W(X){X/t)} para qq termo t
onde Y1,... e Yn são as variáveis, caso existam, que ocorrem em t
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
191
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Resolução em Lógica de Predicados
Temos as seguintes cláusulas que estão implicitamente
universalmente quantificadas
 gosta(luis, Y)  feminino(Y)  tia(Y,Z)
gosta(X, mae)  ama(X, mae)
a resolução actua instanciando em primeiro lugar ambas as cláusulas através
da substituição
 = {Y/mae, X/luis}
de forma a tornar os literais ‘gosta’ complementares:
 gosta(luis, mae)  feminino(mae)  tia(mae,Z)
gosta(luis, mae)  ama(luis, mae)
antes de continuar exactamente como no caso proposicional para obter o
resolvente
 ama(luis, mae)  feminino(mae)  tia(mae,Z)
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
192
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Resolução em Lógica de Predicados
Resumindo, se tivermos
A  A1  …  Am
C  A  C1  …  Cn
a resolução procura um literal no antecedente da implicação e o
mesmo literal no consequente de outra cláusula e, com um passo
da resolução, obtemos
C  A1  …  Am  C1  …  Cn
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
193
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Resolução em Lógica de Predicados
Um literal positivo é representado como
A
(que é o mesmo que dizer A  true)
Um literal negativo é representado como
A
(que é o mesmo que dizer false  A)
Resolução chã para um conjunto C de cláusulas é a aplicação
da resolução proposicional a um conjunto de instanciações chãs
das cláusulas de C.
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
194
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Resolução em Lógica de Predicados
Um unificador para as fórmulas W1 e W2 é a
substituição  tal que W1 = W2.
Um unificador  para duas fórmulas W1 e W2
diz-se um unificador mais geral se e só se, para
todo o unificador  para as fórmulas existe uma substituição 
tal que  = °.
Pode-se estender a noção de unificador a um conjunto de
fórmulas.
Um conjunto de fórmulas diz-se unificável se e só se admite um
unificador.
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
195
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Resolução em Lógica de Predicados
 = {X/a, Y/a} é um unificador para p(X) e p(Y), mas
não é o unificador mais geral.
O unificador mais geral é  = {X/Y}
Ou seja  =  {Y/a}
Mostrar que  =  ° , se  = {Y/a}
As fórmulas p(X, f(Y)) e p(f(U), g(Z)) não são unificáveis.
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
196
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Resolução em Lógica de Predicados
Mudança (ou renomeação) de variáveis
É uma substituição que substitui apenas variáveis por variáveis.
Por exemplo, dadas as fórmulas {p(f(Z), X), p(Y,g(U))}
temos que uma mudança de variáveis é:
 = {Z/Z1, X/X1, Y/Y1, U/U1}, donde obteríamos p(f(Z1), X1) e
p(Y1, g(U1))
Um unificador mais geral é único a menos de uma mudança de
variáveis. Quer dizer, se  e  são unificadores mais gerais
para um conjunto de fórmulas, existe uma mudança de
variáveis  tal que  = °.
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
197
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Resolução em Lógica de Predicados
Dadas as fórmulas {p(f(Z), X), p(Y,g(U))} temos os dois
u.m.g.
 = {X/g(U), Y/f(Z)}
 = {X/g(U1), Y/f(Z1), Z/Z1, U/U1}
A mudança de variáveis  apresentada no exemplo anterior
valida o que foi declarado, ou seja
 = °
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
198
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Unificação
Todo o conjunto unificável admite um unificador mais geral.
Prova
Existe um algoritmo que indica se um dado conjunto é
unificável e, no caso afirmativo, retorna o unificador mais geral.
Esse algoritmo é chamado de unificação.
O algoritmo usa uma pilha S na qual guardamos pares de
termos a unificar, e que iniciamos com os pares <ti, ri>.
Recorre-se ainda a uma variável booleana para indicar a
impossibilidade de unificar as duas expressões.
O unificador mais geral  é construído progressivamente
começando com a identidade.
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
199
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)