{

Árvore de prova sec:2-2}} Uma árvore de prova é uma entidade perfeitamente definida que constitui, por si só, uma prova, intuitivamente evidente, que um átomo é consequência lógica de um programa. Vejamos, primeiro, um exemplo de uma árvore de prova para o problema 1: %%%%%%%%%%%%%%%%%%%%%%%%
0.6cm} {center} { & avo(rosa,ana) @{-}[dl] @{-}[dr] &
progenitor(rosa,luis) @{-}[d]& & progenitor(luis,ana) @{-}[d]
mae(rosa,luis) @{-}[d] & & pai(luis,ana)@{-}[d]
verdade & & verdade} center}
0.6cm} %%%%%%%%%%%%%%%%%%%%%%%% Estando feito o programa {P} (o ``nosso primeiro programa em Prolog''), uma leitura de baixo para cima desta árvore conduz à convicção que o átomo na raiz, {avo(rosa,ana)}, é consequência lógica de {P}, visto que esta leitura (de baixo para cima) segue o sentido dos s{i}mbolos {:-} nas cláusulas em {P} e estes s{i}mbolos são interpretados como implicações. Não vamos dar uma definição formal da noção de {árvore de prova} segundo {P}, mas apenas reter que é uma árvore (finita), orientada, cujos {nós} são constitu{i}dos por átomos, cujas folhas (nós terminais) são constitu{i}das pelos átomos fict{i}cios {verdade} e cujos nós não terminais verificam a seguinte propriedade: a cada nó não terminal corresponde uma instância de uma cláusula do programa {P}, a cabeça da instância da cláusula coincidindo com o átomo contido nesse nó, os átomos do corpo dessa instância de cláusula sendo os átomos que constituem os filhos do nó. No caso em que o corpo é vazio, colocamos o átomo fict{i}cio {verdade} como único filho. Observe-se que toda a sub-árvore de uma árvore de prova é também uma árvore de prova. Por outras palavras, todo o átomo contido num nó de uma árvore de prova é átomo raiz de uma árvore de prova. Por outro lado, uma árvore de prova pode comportar variáveis e então toda a instância de uma árvore de prova é ainda uma árvore de prova. Com as noções introduzidas é poss{i}vel demonstrar o seguinte teorema.
{Teorema:} Um átomo é consequência lógica de {P} se, e somente se, é raiz de uma árvore de prova segundo {P}.
Assim sendo, a notação {CL(P)} é exactamente o conjunto dos átomos que são ra{i}zes de uma árvore de prova segundo {P}. Este resultado pode ser visto como um resultado de equivalência entre um significado lógico e um significado construtivo baseado na noção de prova. Resta agora ver como produzir, de uma maneira efectiva, as árvores de prova, isto é, uma maneira de obter as respostas lógicas a uma questão. %%%%%%%%%%%%%%%%%%