{

Substituição e instância} Usamos a notação $$ s = { {X} {ana}, {Z} {Y}} $$ para designar uma função $s$ do conjunto das variáveis no conjunto dos termos, que à variável {X} associa o termo {ana}, à variável {Z} associa o termo {Y} e deixa inalteradas as outras variáveis. Pondo de parte as questões formais da poss{i}vel confusão entre ``linguagem'' e ``meta-linguagem'', esta função $s$ pode ser definida da maneira habitual: para toda a variável $V$ $$ s(V) = { {tabular}{lcl} {ana} & se & $V = X$
Y & se & $V = Z$
V & se & $V X$ e $V Z$ tabular} . $$ Dizemos que $s$ é uma {substituição}. Uma substituição aplica-se, de um modo natural, a termos, átomos ou cláusulas. Por exemplo, se aplicarmos a substituição $s$ à cláusula {verbatim} avo(X,Z) :- progenitor(X,Y), progenitor(Y,Z). verbatim} obteremos a cláusula {verbatim} avo(ana,Y) :- progenitor(ana,Y), progenitor(Y,Y). verbatim} A esta cláusula resultante chamamos {instância} da primeira cláusula pela substituição $s$. Uma instância por uma substituição, obtém-se substituindo as variáveis pelos termos indicados na substituição. Se $X_1, X_2, ... X_n$ são as únicas variáveis $X$ para as quais $s(X) X$ e se $$ s(X_1)=t_1, s(X_2)=t_2, ... s(X_n)=t_n $$ utilizamos a notação $$ s = { X_1 t_1,..., X_n t_n } $$ A substituição identidade é denotada por ${ }$ e deixa inalterada todas as variáveis, e deste modo cada termo, átomo, cláusula, ... A imagem de um termo (átomo, cláusula) por uma substituição é chamada instância do termo (átomo, cláusula) pela substituição. Note-se que uma instância de uma instância de $t$ é uma instância de $t$. Mais formalmente, a composição de duas substituições, como uma função sobre o conjunto dos termos (átomos, cláusulas) é ainda uma substituição. Estas noções permitem dar um sentido rigoroso à noção de {questão} e {resposta}. Seja {P} um programa e {A} um átomo. Uma {resposta lógica} (segundo {P}) à questão {verbatim} ?- A. verbatim} é uma substituição $s$ tal que {s(A)}, instância de {A} por $s$, é uma consequência lógica de {P}, quer dizer, $s({A}) {CL(P)}$. Segue-se um exemplo para o nosso problema 1: à questão {verbatim} ?- avo(rosa,N). verbatim} uma das respostas lógicas, de acordo com o programa que fizemos, é $$ { N ana } $$