{

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{i}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^{{o}} 1$ e partir do átomo inicial {avo(rosa,N)} correspondente à questão {verbatim} ?- avo(rosa,N). verbatim}
0.6cm} {Etapa ${n^{{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: {verbatim} avo(A1,N1) :- progenitor(A1,B1), progenitor(B1,N1). verbatim} O algoritmo de unificação dá-nos o unificador minimal $$ s_1 = { {A1} {rosa}, {N1} {N} } $$ Notar que pod{i}amos também tomar o outro unificador minimal: $$ { {A1} {rosa}, {N} {N1} } $$ Instanciamos a árvore de prova parcial por $s_1$ 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:
0.6cm} {Etapa ${n^{{o}} 2}$} %%%%%%%%%%%%%%%%%%%%%%%%
0.6cm} {center} { & avo(rosa,N) @{-}[dl] @{-}[dr] &
progenitor(rosa,B1) & & progenitor(B1,N)} center}
0.6cm} %%%%%%%%%%%%%%%%%%%%%%%% 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 {verbatim} progenitor(P2,F2) :- mae(P2,F2). verbatim} O algoritmo de unificação dá-nos $s_2 = { {P2} {rosa}, {F2} {B1} }$. Instanciamos por $s_2$ a árvore de prova parcial e a cláusula, acrescentando os átomos do corpo da cláusula como filhos da folha escolhida. Obtemos:
0.6cm} {Etapa ${n^{{o}} 3}$} %%%%%%%%%%%%%%%%%%%%%%%%
0.6cm} {center} { & avo(rosa,N) @{-}[dl] @{-}[dr] &
progenitor(rosa,B1) @{-}[d]& & progenitor(B1,N)
mae(rosa,B1) & & } center}
0.6cm} %%%%%%%%%%%%%%%%%%%%%%%% {Escolhemos} uma folha. Seja ela {mae(rosa,B1)}. A única cláusula cuja cabeça pode ser unificada com a folha considerada é o facto {verbatim} mae(rosa,luis). verbatim} O unificador é $s_3 = { {B1} {luis} }$. Instanciamos ao mesmo tempo por $s_3$ a árvore e o facto. Neste caso o corpo da cláusula é vazio (facto) pelo que acrescentamos como filho o átomo fict{i}cio $verdade$, obtendo
0.6cm} {Etapa ${n^{{o}} 4}$} %%%%%%%%%%%%%%%%%%%%%%%%
0.6cm} {center} { & avo(rosa,N) @{-}[dl] @{-}[dr] &
progenitor(rosa,luis) @{-}[d] & & progenitor(luis,N)
mae(rosa,luis) @{-}[d] & &
verdade & & } center}
0.6cm} %%%%%%%%%%%%%%%%%%%%%%%% Apenas nos resta a folha {progenitor(luis,N)}. {Escolhamos} uma cláusula (renomeada). Seja ela {verbatim} progenitor(P4,F4) :- pai(P4,F4). verbatim} Um unificador minimal é $s_4 = { {P4} {luis}, {F4} {N} }$. Instanciando a árvore e cláusula por $s_4$, e acrescentando o átomo do corpo da cláusula como filho, obtemos:
0.6cm} {Etapa ${n^{{o}} 5}$} %%%%%%%%%%%%%%%%%%%%%%%%
0.6cm} {center} { & avo(rosa,N) @{-}[dl] @{-}[dr] &
progenitor(rosa,luis) @{-}[d] & & progenitor(luis,N) @{-}[d]
mae(rosa,luis) @{-}[d] & & pai(luis,N)
verdade & & } center}
0.6cm} %%%%%%%%%%%%%%%%%%%%%%%% {Escolhemos} uma cláusula (renomeada) poss{i}vel de instanciar com a folha {pai(luis,N)}. Consideremos, por exemplo, o facto {verbatim} pai(luis,ana). verbatim} O unificador é $s_5 = { N ana }$. Instanciando por $s_5$ e atendendo que a cláusula escolhida é um facto, acrescentamos como filho o átomo fict{i}cio $verdade$, obtendo finalmente a árvore de prova apresentada na secção #_#>sec:2-2}:
0.6cm} {Etapa ${n^{{o}} 6}$} %%%%%%%%%%%%%%%%%%%%%%%%
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} %%%%%%%%%%%%%%%%%%%%%%%% 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 s_4 s_3 s_2 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 {verbatim} ?- A. verbatim} 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{i}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{i}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: ${ {N} {eusebio} }$; 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{i}vel de ser unificada com a folha escolhida.
Como já foi referido, existem duas fontes de não determinismo: {itemize} não determinismo do tipo {f}: escolha da folha; não determinismo do tipo {c}: escolha da cláusula. itemize} É poss{i}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: {verbatim} ?- avo(A,ana), progenitor(A,aldina). verbatim} 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 {verbatim} questao(A) :- avo(A,ana), progenitor(A,aldina). verbatim} e tomar como nova questão o átomo {questao(A)}: {verbatim} ?- questao(A). verbatim}