Construção de uma árvore de prova

Obtemos a noção de árvore de prova parcial a partir da noção de árvore de prova, modificando a condição sobre as folhas. Numa árvore de prova parcial, uma folha pode conter verdade ou um átomo. Uma árvore de prova (total) é uma árvore de prova parcial em que todas as folhas contêm verdade. Existe um algoritmo que, dado um átomo A, constroi, eventualmente, uma árvore de prova com um átomo na raiz que é uma instância de A. Esse algoritmo é ``não determinístico'', na medida que contém escolhas a serem feitas. Vejamos um exemplo que mostra o método. A ideia é considerar o átomo inicial A como constituindo ele mesmo uma árvore de prova parcial e ir depois ``desenvolvendo'' essa árvore de prova parcial pelas suas folhas e instanciando-a. O exemplo consiste em considerar o programa P que fizemos no âmbito do problema $n^{\footnotesize {o}} 1$ e partir do átomo inicial avo(rosa,N) correspondente à questão

         ?- avo(rosa,N).

Etapa $\mathbf{n^{\footnotesize {o}} 1}$ A árvore de prova parcial reduz-se a uma única folha

avo(rosa,N)

Vamos escolher uma cláusula em P para ``pendurar'' filhos a esta folha, mas as variáveis dessa cláusula não deverão ter relação com as da árvore de prova parcial, o que nos leva a substituir a cláusula por uma sua renomeação em relação às variáveis da árvore de prova parcial. De um ponto de vista lógico esta renomeação não tem qualquer reflexo, uma vez que as variáveis de uma cláusula são quantificadas universalmente. Escolhemos uma cláusula (renomeada) cuja cabeça possa ser unificada com a folha avo(rosa,N). Neste caso existe apenas uma possibilidade:

         avo(A1,N1) :- progenitor(A1,B1), progenitor(B1,N1).

O algoritmo de unificação dá-nos o unificador minimal

$\begin{displaymath}s_1 = \left\{ \texttt{A1} \leftarrow \texttt{rosa},\, \texttt{N1} \leftarrow \texttt{N} \right\} \end{displaymath}$

Notar que podíamos também tomar o outro unificador minimal:

$\begin{displaymath}\left\{ \texttt{A1} \leftarrow \texttt{rosa},\, \texttt{N} \leftarrow \texttt{N1} \right\} \end{displaymath}$

Instanciamos a árvore de prova parcial por s₁ assim como a cláusula (renomeada). Por construção a folha da árvore de prova parcial coincide agora com a cabeça da cláusula. Acrescentamos os átomos do corpo da cláusula como filhos da folha, obtendo então uma nova árvore de prova parcial:

Etapa $\mathbf{n^{\footnotesize {o}} 2}$

$\xymatrix{ & avo(rosa,N) \ar@{-}[dl] \ar@{-}[dr] & \\ progenitor(rosa,B1) & & progenitor(B1,N)}$

Vamos escolher uma das folhas desta árvore de prova parcial. Consideremos, por exemplo, a folha progenitor(rosa,B1). De seguida, escolhemos uma cláusula (renomeada) de P cuja cabeça possa ser unificada com a folha escolhida. Consideremos a cláusula

         progenitor(P2,F2) :- mae(P2,F2).

O algoritmo de unificação dá-nos $s_2 = \left\{ \texttt{P2} \leftarrow \texttt{rosa},\, \texttt{F2} \leftarrow \texttt{B1} \right\}$ . Instanciamos por s₂ a árvore de prova parcial e a cláusula, acrescentando os átomos do corpo da cláusula como filhos da folha escolhida. Obtemos:

Etapa $\mathbf{n^{\footnotesize {o}} 3}$

$\xymatrix{ & avo(rosa,N) \ar@{-}[dl] \ar@{-}[dr] & \\ progenitor(rosa,B1) \ar@{-}[d]& & progenitor(B1,N) \\ mae(rosa,B1) & & }$

Escolhemos uma folha. Seja ela mae(rosa,B1). A única cláusula cuja cabeça pode ser unificada com a folha considerada é o facto

         mae(rosa,luis).

O unificador é $s_3 = \left\{ \texttt{B1} \leftarrow \texttt{luis} \right\}$ . Instanciamos ao mesmo tempo por s₃ a árvore e o facto. Neste caso o corpo da cláusula é vazio (facto) pelo que acrescentamos como filho o átomo fictício verdade, obtendo

Etapa $\mathbf{n^{\footnotesize {o}} 4}$

$\xymatrix{ & avo(rosa,N) \ar@{-}[dl] \ar@{-}[dr] & \\ progenitor(rosa,luis) \... ...[d] & & progenitor(luis,N) \\ mae(rosa,luis) \ar@{-}[d] & & \\ verdade & & }$

Apenas nos resta a folha progenitor(luis,N). Escolhamos uma cláusula (renomeada). Seja ela

         progenitor(P4,F4) :- pai(P4,F4).

Um unificador minimal é $s_4 = \left\{ \texttt{P4} \leftarrow \texttt{luis},\, \texttt{F4} \leftarrow \texttt{N} \right\}$ . Instanciando a árvore e cláusula por s₄, e acrescentando o átomo do corpo da cláusula como filho, obtemos:

Etapa $\mathbf{n^{\footnotesize {o}} 5}$

$\xymatrix{ & avo(rosa,N) \ar@{-}[dl] \ar@{-}[dr] & \\ progenitor(rosa,luis) \... ...,N) \ar@{-}[d] \\ mae(rosa,luis) \ar@{-}[d] & & pai(luis,N) \\ verdade & & }$

Escolhemos uma cláusula (renomeada) possível de instanciar com a folha pai(luis,N). Consideremos, por exemplo, o facto

         pai(luis,ana).

O unificador é $s_5 = \left\{ N \leftarrow ana \right\}$ . Instanciando por s₅ e atendendo que a cláusula escolhida é um facto, acrescentamos como filho o átomo fictício verdade, obtendo finalmente a árvore de prova apresentada na secção 2.2:

Etapa $\mathbf{n^{\footnotesize {o}} 6}$

$\xymatrix{ & avo(rosa,ana) \ar@{-}[dl] \ar@{-}[dr] & \\ progenitor(rosa,luis)... ... mae(rosa,luis) \ar@{-}[d] & & pai(luis,ana)\ar@{-}[d]\\ verdade & & verdade}$

O processo de construção de uma árvore de prova é, então, um processo por aproximações sucessivas. Se acharmos a composição dos unificadores usados em cada etapa, obtemos uma substituição s. No exemplo precedente, $s = s_5 \circ s_4 \circ s_3 \circ s_2 \circ s_1$ . Esta substituição verifica a seguinte propriedade: o átomo da raiz da árvore de prova é uma instância s(A) do átomo inicial A. A s chamamos resposta calculada à questão

         ?- A.

Resulta que toda a resposta calculada é uma resposta lógica. O que falta examinar é a completude do algoritmo de construção de árvores de prova, isto é, se poderemos obter deste modo todas as respostas lógicas. O algoritmo que vimos é não determinístico. No exemplo considerado fomos escolhendo quer as folhas quer as cláusulas. Se tivessemos escolhido as folhas de outra maneira, mas conservando as mesmas escolhas de cláusulas, teríamos obtido a mesma árvore de prova. Por outro lado, a escolha diferente das cláusulas ter-nos-ia levado a uma outra árvore de prova e a uma outra resposta calculada: $\left\{ \texttt{N} \leftarrow \texttt{eusebio} \right\}$ ; ou então a um impasse, quer dizer, a uma impossibilidade de continuar a construção, por falta de uma cláusula cuja cabeça fosse passível de ser unificada com a folha escolhida.
Como já foi referido, existem duas fontes de não determinismo:

não determinismo do tipo f: escolha da folha;
não determinismo do tipo c: escolha da cláusula.

É possível formular rigorosamente, e demonstrar, um resultado de completude que diz que, para obter todas as respostas lógicas, é suficiente fixar, arbitrariamente, as escolhas do tipo f e tentar todas as escolhas do tipo c.
Observe-se, por último, que foi apenas para simplificar que representámos uma questão por um átomo. Chamamos alvo a uma sucessão finita de átomos. Uma questão pode ser representada por um alvo. Um exemplo de uma questão para o nosso problema 1 pode ser:

         ?- avo(A,ana), progenitor(A,aldina).

Esta questão significa: ``Quem são os avós de ana que são também progenitores de aldina?''. Poderemos sempre considerar uma questão reduzida a um só átomo. Para isso basta acrescentar uma cláusula adequada ao programa. Para o exemplo acima, podemos acrescentar a cláusula

         questao(A) :- avo(A,ana), progenitor(A,aldina).

e tomar como nova questão o átomo questao(A):

         ?- questao(A).

Delfim F. Marado Torres
1999-03-16