{

Unificação} O átomo contido num nó não terminal de uma árvore de prova, é uma instância de uma cabeça de cláusula. Excluindo a raiz, esse átomo é também uma instância de um átomo do corpo de uma cláusula. A construção de uma árvore de prova, em grosso modo, reduz-se à procura de instâncias comuns a dois átomos. É este facto que motiva as considerações que se seguem. Para explicarmos o conceito de unificação, na sua forma mais geral, e também para estarmos de acordo com a funcionalidade do Prolog, vamos, antes de mais, generalizar o conceito de átomo. Tinhamos dito que um átomo escreve-se com um s{i}mbolo de predicado e um número de termos igual à aridade do s{i}mbolo do predicado em questão e que estes termos constituiam os chamados argumentos do átomo. Vamos agora permitir (definição recursiva!) que os argumentos possam ser, eles mesmo, átomos. Dois átomos $atomo_1$ e $atomo_2$ são {unificáveis}, se existir uma substituição {s} tal que $s(atomo_1) = s(atomo_2)$. Nesse caso dizemos que $s$ é um {unificador} de $atomo_1$ e $atomo_2$. Por exemplo os átomos $atomo_1 = p(X,b)$ e $atomo_2 = p(a,Y)$ são unificáveis pelo unificador $ s = {X a, Y b}$. Uma constante é apenas unificável com ela própria e com uma variável. Intuitivamente, um unificador do $atomo_1$ e do $atomo_2$, é uma substituição que consegue ``instanciar'' suficientemente as variáveis de modo a satisfazer a equação $atomo_1 = atomo_2$. Um {unificador minimal}, é um unificador que instancia o menos poss{i}vel as variáveis. Por exemplo os dois átomos $atomo_1 = p(X,Y)$ e $atomo_2 = p(Y,X)$ são unificáveis por $s_1 = {YX}$, por $s_2 = {XY}$, por $s_3 = {Xa,Ya}$, ...mas $s_1$ e $s_2$ são os unificadores minimais. Formalmente, o unificador $s$ é minimal se, para todo o unificador $s'$, existe uma substituição $s''$ tal que $s' = s'' s$ (composição de substituições). Pode-se mostrar que se existir um unificador entre dois átomos, então existe um unificador minimal. Também é poss{i}vel demonstrar que se {X} é uma variável e {atomo} um átomo, então {atomo} e {X} são unificáveis se, e somente se, {atomo} não contiver a variável {X} (quando a varável {X} não tem {ocorrência} em {atomo}). Existe um algoritmo (algoritmo de Robinson) que, dados dois átomos, calcula um unificador minimal, se os os dois átomos são unificáveis, ou então termina com a indicação da impossibilidade de unificação. Seguem-se dois exemplos simples que ilustram o método. Ajuda representar os átomos na forma de árvore. A ideia é tentar construir o unificador por aproximações sucessivas, por composição de substituições. Em cada etapa procuramos uma variável que é uma folha numa das árvores e tentamos unificá-la com a sub-árvore correspondente na outra árvore. Nos esquemas que se seguem, essas variáveis e essas sub-árvores são envoltas com uma curva fechada.
0.6cm} {Primeiro Exemplo:} $atomo_1 = p(X,Y)$, $atomo_2 = p(Y,g(a))$
0.6cm} {Etapa ${n^{{o}} 1}$}
{center} %%%%%%%%%%%%%%%%%%%%%%%% { & {{atomo_1}} & & & & {{atomo_2}} &
& p @{-}[dl] @{-}[dr] & & & & p @{-}[dl] @{-}[dr] &
*++[o][F-]{X} & & Y & & *++[o][F-]{Y} & & g @{-}[d]
& & & & & & a} %%%%%%%%%%%%%%%%%%%%%%%% center} $s_1 = { X Y }$ %%%%%%%%%%%%%%%%%%%%%%%%
0.6cm} {Etapa ${n^{{o}} 2}$} {center} %%%%%%%%%%%%%%%%%%%%%%%% { & {{s_1(atomo_1)}} & & & & {{s_1(atomo_2)}} &
& p @{-}[dl] @{-}[dr] & & & & p @{-}[dl] @{-}[dr] &
Y & & *++[o][F-]{Y} & & Y & & g @{-}[d]
& & & & & & a "3,7"."4,7"*[e][F-]{} } %%%%%%%%%%%%%%%%%%%%%%%% center} $s_2 = { Y g(a) }$
0.6cm} %%%%%%%%%%%%%%%%%%%%%%%% {Etapa ${n^{{o}} 3}$} {center} %%%%%%%%%%%%%%%%%%%%%%%% { & {{s_2(s_1(atomo_1))}} & & & & {{s_2(s_1(atomo_2))}} &
& p @{-}[dl] @{-}[dr] & & & & p @{-}[dl] @{-}[dr] &
g @{-}[d] & & g @{-}[d] & & g @{-}[d] & & g @{-}[d]
a & & a & & a & & a } %%%%%%%%%%%%%%%%%%%%%%%% center}
0.6cm} {Conclusão:} unificador minimal dado por $$ s_2 s_1 = { X g(a), Y g(a) } $$ {Segundo Exemplo:} $$ atomo_1 = p(Y,h(a,X)),     atomo_2 = p(X,h(Y,b)) $$
0.6cm} {Etapa ${n^{{o}} 1}$} {center} %%%%%%%%%%%%%%%%%%%%%%%% { & {{atomo_1}} & & & & & {{atomo_2}} & &
& p @{-}[dl] @{-}[dr] & & & & & p @{-}[dl] @{-}[dr] & &
*++[o][F-]{Y} & & h @{-}[dl] @{-}[dr] & & & *++[o][F-]{X} & & h @{-}[dl] @{-}[dr] &
& a & & X & & & Y & & b} %%%%%%%%%%%%%%%%%%%%%%%% center} $s_1 = { Y X }$
0.6cm} %%%%%%%%%%%%%%%%%%%%%%%% {Etapa ${n^{{o}} 2}$} {center} %%%%%%%%%%%%%%%%%%%%%%%% { & {{s_1(atomo_1)}} & & & & & {{s_1(atomo_2)}} & &
& p @{-}[dl] @{-}[dr] & & & & & p @{-}[dl] @{-}[dr] & &
X & & h @{-}[dl] @{-}[dr] & & & X & & h @{-}[dl] @{-}[dr] &
& *++[o][F-]{a} & & X & & & *++[o][F-]{X} & & b} %%%%%%%%%%%%%%%%%%%%%%%% center} $s_2 = { X a }$
0.6cm} %%%%%%%%%%%%%%%%%%%%%%%% {Etapa ${n^{{o}} 3}$} {center} %%%%%%%%%%%%%%%%%%%%%%%% { & {{s_2(s_1(atomo_1))}} & & & & & {{s_2(s_1(atomo_2))}} & &
& p @{-}[dl] @{-}[dr] & & & & & p @{-}[dl] @{-}[dr] & &
a & & h @{-}[dl] @{-}[dr] & & & a & & h @{-}[dl] @{-}[dr] &
& a & & *++[o][F-]{a} & & & a & & *++[o][F-]{b}} %%%%%%%%%%%%%%%%%%%%%%%% center}
0.6cm} %%%%%%%%%%%%%%%%%%%%%%%% {Conclusão:} os átomos não são unificáveis (a constante $a$ não unifica com a constante $b$).
Dois átomos $atomo_1$ e $atomo_2$ são duas {variantes}, se podermos passar de um ao outro por uma simples mudança do nome das variáveis (duas variáveis distintas mudadas sempre por duas variáveis distintas). Por outro lado, $atomo_2$ é uma {renomeação} do $atomo_1$, em relação a um conjunto $V_1$ de variáveis, se $atomo_2$ é uma variante do $atomo_1$ e se $atomo_2$ não contiver nenhuma variável em $V_1$. As nocões de unificação e de renomeação, definidas para átomos, estendem-se, da maneira natural, para as cláusulas.