Lógica de
Predicados
Teorema de Herbrand
e Unificação
Desejo antigo...

Encontrar um procedimento geral de
decisão para verificar a validade (ou
inconsistência) de uma fórmula



Leibniz (1700s)
Peano (1700s-1800s)
Hilbert na década de 20
Church e Turing[1936] ->
impossível!!



Não existe um procedimento de decisão
para verificar a validade de fórmulas da
lógica de predicados 
Mas existem métodos de prova que
podem verificar se uma fórmula é válida
se realmente ela for!! 
Para fórmulas inválidas, esses
procedimentos são indecidíveis 
Herbrand (1930)



Uma fórmula válida é verdadeira sob todas as suas
interpretações
Herbrand desenvolveu um algoritmo para encontrar
uma interpretação que pode invalidar uma fórmula!
No entanto, se ela é válida, nenhuma dessas
interpretações pode existir


O algoritmo termina após um número finito de tentativas!
O método de Herbrand é a base para muitos
métodos modernos de prova automática
Reduzindo o problema



Um conjunto S de cláusulas é insatisfatível
sse for falso sob todas as interpretações
sobre todos os domínios
Mas... é inconveniente e impossível
considerar todas as interpretações sobre
todos os domínios
Idéia: usar um domínio especial H, tal que S
é insatisfatível se e somente se S é falso sob
todas as interpretações sobre H

H é o universo de Herbrand de S
Universo de Herbrand de um
Conjunto de Cláusulas (H)

Se Ho é o conjunto de constantes que
aparecem em S

Se nenhuma constante aparece em S


então Ho é formado por uma única constante,
Ho={a}
Se f é um símbolo funcional n-ário ocorrendo
em S, e

se t1, ...,tn são termos que pertencem a H, então o
termo f(t1, ...,tn) também pertence a H
Exemplos de universos de
Herbrand








S = {P(x)  Q(x), P(x)}
H0 = H = {a}
S = {P(a), P(x)  P(f(x))}
H0 = {a}
H1 = {a, f(a)}
H2 = {a, f(a), f(f(a))}
...
H = H = {a, f(a), f(f(a)), f(f(f(a))), ... }
Base de Herbrand


Um termo-base é um elemento de H
Uma base de Herbrand para S é o conjunto
B(S) de todas as fórmulas atômicas da forma
P(t1, ...,tn)





P é um símbolo predicativo ocorrendo em S
t1, ...,tn termos-base
Exemplo: S = {P(x)  Q(x), R(f(y))}
H = {a, f(a), f(f(a)), ... }
B(S) = {P(a), Q(a), R(a), P(f(a)), Q(f(a)),
R(f(a)), ...}
Interpretação de Herbrand

Uma interpretação I para S é uma
interpretação de Herbrand para S sse



o domínio U de I é H
para cada constante a de S, aI = a
para cada função f de S, fI(t1, ...,tn) =
f(t1, ...,tn),


para cada t1, ...,tn  H(S)
Também chamada de H-interpretação
Exemplos de H-interpretações

S = {P(x)  Q(x), R(f(y))}
H = {a, f(a), f(f(a)), ... }
B(S) = {P(a), Q(a), R(a), P(f(a)), Q(f(a)), R(f(a)), ...}

Algumas H-interpretações para S:





I1 = {P(a), Q(a), R(a), P(f(a)), Q(f(a)), R(f(a)), ... }
I2 = {P(a), Q(a), R(a), P(f(a)), Q(f(a)),
R(f(a)), ... }
I3 = {P(a), Q(a),  R(a), P(f(a)),Q(f(a)), R(f(a)),...}
H-interpretação correspondente

Dada uma interpretação I, uma H-interpretação I*
correspondente a I é uma H-interpretação em que






Sendo h1, ..., hn elementos de H (o universo Herbrand
de S)
Sendo cada hi mapeado para alguma variável di
Se é atribuído a P(d1, ... , dn) V(F) por I,
então para P(h1, ... , hn) também é atribuído V(F) em I*
Se uma interpretação I sobre algum domínio D
satisfaz um conjunto de cláusulas S, então qualquer
H-interpretação I* correspondente a I também
satisfaz S
Exs: I1 e I2
Árvores semânticas

Encontrar uma prova para um conjunto
de cláusulas S é


Árvores semânticas completas



gerar uma árvore semântica fechada!
contém todas as possibilidades
Em LPO, as árvores são infinitas...
Mas, se S é insatisfatível, uma árvore
semântica sobre H é fechada e finita!
Árvore semântica


S = {P(x), Q(f(x))}
B = {P(a), Q(a), P(f(a)), Q(f(a)), P(f(f(a))),...}.
Árvore semântica completa


P(a)
P(a)
S = {P(x), P(a)}
B = {P(a)}
Exemplos de árvores
semânticas completas
Nós de falha


S = {P, Q v R, P v Q, P v R}
B = {P, Q, R}.
Árvore semântica fechada


S = {P(x),
P(x) v Q(f(x)),
Q(f(a))}
B = {P(a), Q(a),
P(f(a)), Q(f(a)), ...}
Teorema de Herbrand



Um conjunto de cláusulas é insatisfatível sse há
um conjunto finito insatisfatível de instânciasbase de cláusulas de S
Reduz o problema da insatisfatibilidade de um
conjunto de cláusulas ao problema de gerar um
conjunto finito de instâncias básicas das
cláusulas do conjunto que seja insatisfatível
Tal conjunto sempre existirá se S for
insatisfatível

...mas poderá não existir em caso contrário.
Método de Herbrand




1. Dado um conjunto S de cláusulas,
gere todos os conjuntos finitos S0, S1,
..., Sn, ... de instâncias-base
2. Para cada conjunto Si gerado, teste
se Si é insatisfatível
3. Pare com SIM, se Si é insatisfatível
4. Pare com NÃO, se não houver novos
conjuntos a gerar
Decidibilidade

Esse procedimento:





sempre pára com SIM quando S for insatisfatível
nunca pára quando S for satisfatível e existir um conjunto
infinito de instâncias básicas de cláusulas de S
sempre pára com NÃO quando S for satisfatível mas o
conjunto de instâncias básicas de cláusulas de S é finito
Procedimento de decisão parcial para o problema
da insatisfatibilidade de conjunto de cláusulas
Procedimento de decisão para o problema da
insatisfatibilidade de conjunto de cláusulas cujo
conjunto de instâncias básicas é finito
Implementação de Gilmore (60)



S = {P(a), ~P(x)  Q(f(x)), ~Q(f(a))}
H0 = {a}
Geram-se todos os Si (método multiplicativo)
S0 = P(a) & (~P(a)  Q(f(a))) & ~Q(f(a))
= ((P(a) & ~P(a))  (P(a) & Q(f(a)))) & Q(f(a))
= (P(a) & ~P(a) & ~Q(f(a)))  (P(a) & Q(f(a)) &
~Q(f(a)))
=
F

F
=
F

Avaliação do algoritmo



MUITO INEFICIENTE!!!
Ordem de 2n , onde n é o número de
instâncias-base
Imagine com 500 instâncias...
Algoritmo de Davis-Putnam
M .Davis, H. Putnam, “A computing procedure for quantification theory", J. of ACM,
Vol. 7, pp. 201-214, 1960



Iterativamente escolhe uma variável até que não haja mais variáveis
INSAT se chegarmos à cláusula vazia
Joga fora cláusulas resolvidas depois de cada iteração
(a + b + c)(b + c’ + f’)(b’ + e)
(a + b) (a + b’) (a’ + c)(a’ + c’)
(a + c + e)(c’ + e + f’)
(a) (a’ + c)(a’ + c’)
(a + e + f’)
(c)(c’)
SAT
()
INSAT
Problemas de explosão de memória!
Para resolver isso: Unificação




2 fórmulas são unificáveis sse existir
uma substituição que, se aplicada a
ambas, torna-as iguais
Como unificar??
Fazendo substituições inteligentes de
variáveis nas 2 fórmulas
Existe um bom algoritmo para isso...
Substituição




É um conjunto O={x1<-t1, ..., xn<-tn}
xi é variável, ti termo e xi<>ti
xi<>xj, com i<>j
Existe substituição vazia ({})
Aplicação de substituição

S é uma expressão e O uma substituição


A aplicação de O em S (SO) é o conjunto
obtido de S substituindo simultaneamente:


O={x1<-t1, ..., xn<-tn}
Todas as ocorrências xi por ti
Se O={}, SO=S
Exemplo








C1 = {p(y1), q(y1,z,x)}
C2 = {p(x), q(w), r(w,y1,z,x,z)}
O = {y1w, wg(a,z,x), xw}
A aplicação de O em C1 e C2 é
C1O= {p(w), q(w,z,w)}
C2O = {p(w), q(g(a,z,x)), r(g(a,z,x),w,z,w,z)}
C1 e C2 não tinham literais complementares...
Mas C1O e C2O têm!
Composição de substituições


Dadas 2 substituições O1 e O2
A composição O1O2 deve manter a
propriedade S(O1O2) = (SO1)O2




S é um conjunto de expressões
O1={xy}, O2={yb}, S={p(x,y)}
S(O1)O2 = (p(x,y){xy}){yb}=p(b,b)
S(O1O2) = p(x,y){xy,yb}=p(y,b)!!
Como resolver??

Antes de substituir {x<-y} e {y<-b}




Aplicar {y<-b} nos termos y que ocorre em O1
({x<-y})
O1O2={x<-y{y<-b},y<-b}={x<-b,y<-b}
O3= {x<-w} e O4= {w<-x}
O3O4=???
Composição de substituições



O3O4={x<-w{w<-x},w<-x}=
{x<-x,w<-x} = {w<-x}
O5= {x<-a} e O6= {x<-b}
O5O6={x<-a{x<-b},x<-b}=
{x<-a,x<-b} = {x<-a}
Composição de substituições



O1={x1<-t1,...xn<-tn}
O2={y1<-s1,...ym<-sm}
Algoritmo para O1O2:



1- Construa F={x1<-t1O2,...,xn<-tnO2, y1<s1,...ym<-sm}
2- Elimine as substituições yi si quando yi=xj
3- Elimine as substituições xi tiO2 quando
xi=tiO2
Exemplo de composição
O1={xf(y),wz,zx} e
O2={yw,xz,zw}, O1O2=?
 O1O2={xf(y)O2,wzO2,zxO2,
yw,xz,zw} (1)
={xf(w),ww,zz, yw,xz,zw}
={xf(w),ww,zz, yw} (2: xz e zw
foram eliminadas; x e z estão em O1)
={xf(w), yw} (3)

Propriedades da composição

O1{}={}O1=O1
(CO1)O2=C(O1O2)
O1(O2O3)=(O1O2)O3

Provadas por indução


Gerando complementares





C1={p(x)} e C2={p(a)} não possuem
literais complementares
Com O1={xa}
C1O1={p(a)} e C2O2={p(a)} com
literais complementares
C3={p(f(x),y,x)} e C4={p(z,g(z),a)}
O2=?? | C3O2=C4O2
Expressões unificáveis

Um conjunto de expressões é unificável se
existir uma substituição O que faça SO=1





O é unificador de S
Ex: S={p(x,y),p(w,x)}
O1={xw, yx} é unificador de S
O2={xa, ya, wa} também
O1 é mais geral que O2



O2, usando a, é mais específica
O2 pode ser obtida de O1
O2=O1{wa,xa}
Unificador mais geral

Se O é unificador de S, ele é o mais
geral se para qualquer unificador Oi





Exista uma substituição F | Oi=OF
Pode ter mais de um...
O1={xw,yg(f(w)),zf(w)} unifica
S={p(f(x),y,x),p(z,g(z),w)}
O2={xa,wa,yg(f(a)),zf(a)} tb!
O1 é mais geral pois O2=O1{wa}
Conjunto de diferenças



Dado S={A1,...An}, um conjunto de
expressões, o conjunto de diferenças é
achado pelo algoritmo
1-Pegue o primeiro símbolo de cada
expressão Ai
2-Se todos os símbolos coincidem, passe para
o próximo símbolo


Senão o conjunto de diferenças é D={E1,...,En}
D pode ser vazio
Exemplo de conjunto de
diferenças



S={p(f(x),y,x),p(z,g(z),a)}
D1={f(x),z}
D2=...
Unificação



Dado um conjunto de expressões S, se S é
unificável, acha-se um Unificador mais geral (ou
indica-se a impossibilidade) fazendo:
1- k=0, O0={}
2-Se SOk=1, Ok é este unificador


Senão ache o conjunto de diferenças Dk de SOk
3-Se existe uma variável x e um termo t em Dk de
forma que x não ocorra em t, então faça
Ok+1=Ok{xt} e incremente k

Se não existir, S não é unificável
Exemplo de unificação














S={p(f(x),y,x), p(z,g(z),w)}
k=0, O0={}, SO0=S <>1, D0={f(x),z}
z não ocorre em f(x), O1=O0{zf(x)}
k=1, O1={}{zf(x)}={zf(x)}
SO1={p(f(x),y,x), p(f(x), g(f(x)),w)}
SO1<>1, D1={y,g(f(x))}
y não ocorre em g(f(x))
O2={zf(x)}{yg(f(x))} ={zf(x),yg(f(x))}, k=2
SO2={p(f(x),g(f(x)),x), p(f(x), g(f(x)),w)} <> 1
D2={x,w}
x não ocorre em w, O3={zf(x)}{yg(f(x))}{xw}
O3={zf(w)}{yg(f(w)),xw}, k=3
SO3={p(f(w), g(f(w)),w)} = 1
O3 é o unificador mais geral
Exemplo não-unificável




S={p(f(x)),p(x)}
D0={f(x),x} e x ocorre em f(x)
Se continuamos ??
Prolog normalmente não testa a
ocorrência, para dar mais eficiência
Cenas dos próximos capítulos
Agora que temos a
unificação, a resolução terá
um passo só...