Fundamentos da Programação em Lógica

A programação lógica é um paradigma de programação no qual um programa corresponde à especificação de um problema de forma declarativa, o que contrasta com outros paradigmas de programação em que são os detalhes correspondentes ao algoritmo que definem a solução do problema.

Por uma questão meramente ligada à eficiência, utilizamos variações especiais de cláusulas e de resolução, as cláusulas de Horn e a resolução SLD, abordadas mais à frente.

Cláusulas de Horn

Cláusulas que contêm, no máximo, um literal positivo (isto é, não negado). Se existir, esse literal positivo será a cabeça da cláusula. Quaisquer literais negativos que possam existir farão parte do corpo da cláusula. São exemplos $\{C, \neg P_{1}, \neg P_{2}\}, \{C\}, \{\neg P_{1}, \neg P_{2}\}$ e $\{\}.$

Dada a equivalência entre $\alpha \to \beta$ e a cláusula de Horn $\{\neg \alpha, \beta\}$, é vulgar escrever cláusulas de Horn sem ser na forma usual de cláusula (com as chavetas). Podemos representar cláusulas com o símbolo $\leftarrow$, com o corpo da cláusula à direita e a cabeça à esquerda. A cláusula vazia é representada por $\square$ (sim, é um quadrado).
Desta feita, os exemplos apresentados anteriormente podem ser apresentados tais que:

As cláusulas de Horn são divididas em quatro tipos:

• Regras/implicações, onde tanto a cabeça como o corpo contêm literais;
• Afirmações/factos, cláusulas onde o corpo não tem literais mas a cabeça sim (pode pensar-se, de modo extremamente informal, da mesma maneira que olhamos para um teorema);
• Objetivos, cláusulas cuja cabeça é vazia mas o corpo contém pelo menos um literal;
• Cláusula vazia.

Se repararmos, os exemplos dados anteriormente são, respetivamente, exemplos de cada um destes tipos.

Tanto as regras como as afirmações chamam-se também cláusulas determinadas (do inglês definite clauses, referindo-se à sua natureza por serem as únicas onde a cabeça contém um literal). São elas que vão constituir os nossos programas em Prolog!

Em resolução com cláusulas de Horn, pelo menos um dos resolventes tem de ser uma cláusula determinada, visto que só estas contêm literais positivos (caso contrário nem sequer seria possível aplicar a resolução).

Programas

Em programação em lógica, um programa é qualquer conjunto finito de cláusulas determinadas; um objetivo, aqui, corresponde a uma cláusula cujas instâncias se pretendam derivar a partir desse programa. Um programa pode ser, por exemplo:

Um objetivo pode ser, por exemplo:

Num programa, o conjunto de todas as cláusulas cuja cabeça corresponde a um literal contendo a letra de predicado $P$ diz-se a definição de $P$ - a definição do predicado $P$, portanto.

Em relação ao exemplo acima, a definição de $Ant$ seria dada por:

Uma definição de predicado que contenha apenas cláusulas fechadas, isto é, sem variáveis, chama-se uma base de dados para esse predicado (precisamente porque não está dependente de nada, são literalmente dados que temos sobre o predicado em questão).

Ainda em relação ao exemplo anterior, a base de dados de $AD$ pode ser dada por:

Resolução SLD

Do inglês Linear Resolution with Selection Function and Definite clauses. É uma estratégia de resolução linear aplicável a cláusulas determinadas (isto é, com cabeça), em conjunto com uma função de seleção, a qual dentro dos possíveis literais aplicáveis de acordo com a resolução escolhe um literal (de modo determinístico).

Esta estratégia é utilizada devido ao princípio da resolução usual não ser determinístico - não há um caminho específico por onde ir. Para além da resolução "normal", o algoritmo de unificação também não é determinístico.

Escolhido o literal, é escolhida também uma cláusula do programa cuja cabeça unifique com o literal escolhido - regra de procura. Este passo é muito importante, porque caso não a apliquemos corretamente podemos correr o risco da prova ser infinita (ou pelo menos muito mais longa do que precisa de ser).

De um modo não rigoroso, a resolução SLD encontra a resposta de um programa a um objetivo, substituindo sucessivamente cada literal no objetivo pelo corpo de uma cláusula cuja cabeça seja unificável com o objetivo escolhido. O processo é sucessivamente repetido até que ou não existam mais sub-objetivos ou quando nenhum dos restantes sub-objetivos for unificável com a cabeça de nenhuma das cláusulas do programa.

Resta ainda definir refutação SLD e resposta calculada:

• Refutação SLD - uma prova SLD diz-se refutação SLD caso o seu último elemento seja a cláusula vazia, $\square$.

• Resposta Calculada - sendo $\Delta$ um programa, $\alpha$ um objetivo e $S$ uma função de seleção. Se a prova SLD para $\alpha$ usando $\Delta$ for finita, $[\gamma_{0}, \dots, \gamma_{n}]$ (sequência de objetivos), a composição das substituições $s_{0},\dots,s_{n-1}$ restringida às variáveis que ocorrem em $\alpha~(s_{0} \circ \dots \circ s_{n-1})|_{vars(\alpha)}$, diz-se uma resposta calculada de $\Delta$ a $\alpha$ via $S$. Diz-se também que $n$ é o comprimento da prova SLD.

Exemplo - Resolução SLD

No exemplo seguinte, temos uma resolução SLD, com objetivo $\leftarrow Ant(Sr.B, Bart)$, não tendo sub-objetivos. Assim sendo, procuramos a sua resolução com uma cabeça de uma cláusula do programa. Escolhemo-la, aplicamos o unificador e temos agora o resultado dessa resolução - um objetivo com dois sub-objetivos. Assim vamos prosseguindo até uma altura em que temos $AD(Sr.B, Marge)$ tanto no corpo como na cabeça das cláusulas que restam como objetivo e programa. Assim sendo, chegamos à cláusula vazia, concluindo que estamos na verdade na presença de uma refutação SLD.

Nesta prova, temos:

$$\begin{aligned} \gamma_{0} & = \quad \leftarrow Ant(Sr.B, Bart)\\ \gamma_{1} & = \quad \leftarrow Ant(Sr.B, y), AD(y, Bart)\\ \gamma_{2} & = \quad \leftarrow Ant(Sr.B, Marge)\\ \gamma_{3} & = \quad \leftarrow AD(Sr.B, Marge)\\ \gamma_{4} & = \quad \square \end{aligned}$$

A resposta calculada é, então:

$$(\{Sr.B/x, Bart/z\} \circ \{Marge/y\} \circ \{Sr.B/x, Marge/y\} \circ \epsilon)|_{\{\}} = \epsilon$$

Árvores SLD

A mesma função de seleção oferece várias alternativas para a construção de uma refutação SLD, consoante a cláusula escolhida. As árvores SLD são úteis para mostrar todas as alternativas em simultâneo.

Tenhamos o programa:

e o objetivo:

Como podemos observar, existem dois nós bem sucedidos e um falhado, sem qualquer ramo infinito.

Resta ainda enunciar uma propriedade muito importante, a independência da função de seleção: tendo um programa $\Delta$ e um objetivo $\alpha$, independentemente da função de seleção, todas as árvores SLD de $\Delta$ e $\alpha$ têm o mesmo número (finito ou infinito) de ramos bem sucedidos.