Árvore de prova

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:

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ímbolos :- nas cláusulas em P e estes sí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ídos por átomos, cujas folhas (nós terminais) são constituídas pelos átomos fictí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í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í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í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.