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,¬P1,¬P2},{C},{¬P1,¬P2}\{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:

CP1,P2CP1,P2.C \leftarrow P_{1}, P_{2}\\ C \leftarrow\\ \leftarrow P_{1}, P_{2}\\ \square.

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).

1Ant(x,y)AD(x,y)Prem2Ant(x,z)Ant(x,y),AD(y,z)Prem3AD(Marge,Bart)Prem4AD(Sr.B,Marge)Prem5Ant(Sr.B,Bart)Prem6Ant(Sr.B,Marge)Res,(1,4),{Sr.B/x,Marge/y}7Ant(Sr.B,z)AD(Marge,z)Res,(2,6),{Sr.B/x,Marge/y}8Ant(Sr.B,Bart)Res,(3,7),{Bart/z}9Res,(5,8),ϵ\def\arraystretch{1.5} \begin{array}{lll} 1 & Ant(x, y) \leftarrow AD(x, y) && Prem\\ 2 & Ant(x, z) \leftarrow Ant(x, y), AD(y, z) && Prem\\ 3 & AD(Marge, Bart) \leftarrow && Prem\\ 4 & AD(Sr.B, Marge) \leftarrow && Prem\\ 5 & \leftarrow Ant(Sr.B, Bart) && Prem\\ 6 & Ant(Sr.B, Marge) \leftarrow && Res, (1,4), \{Sr.B/x, Marge/y\}\\ 7 & Ant(Sr.B, z) \leftarrow AD(Marge, z) && Res, (2, 6), \{Sr.B/x, Marge/y\}\\ 8 & Ant(Sr.B, Bart) \leftarrow && Res, (3, 7), \{Bart/z\}\\ 9 & \square && Res, (5, 8), \epsilon \end{array}

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:

Ant(x,y)AD(x,y)Ant(x,z)Ant(x,y),AD(y,z)AD(Marge,Bart)AD(Sr.B,Marge)Ant(x, y) \leftarrow AD(x, y)\\ Ant(x, z) \leftarrow Ant(x, y), AD(y, z)\\ AD(Marge, Bart) \leftarrow\\ AD(Sr.B, Marge) \leftarrow\\

Um objetivo pode ser, por exemplo:

Ant(Sr.B,Bart)\leftarrow Ant(Sr.B, Bart)

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

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

{Ant(x,y)AD(x,y),Ant(x,z)Ant(x,y),AD(y,z)}\{Ant(x, y) \leftarrow AD(x, y), Ant(x, z) \leftarrow Ant(x, y), AD(y, z)\}

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 ADAD pode ser dada por:

{AD(Marge,Bart),AD(Sr.B,Marge)}\{AD(Marge, Bart) \leftarrow, AD(Sr.B, Marge) \leftarrow \}

Definições a reter

  • Resposta de um programa a um objetivo - Sendo Δ\Delta um programa e α\alpha um objetivo, uma resposta de Δ\Delta ao objetivo α\alpha é uma substituição ss para as variáveis de α\alpha.

  • Restrição de uma substituição a variáveis - Sendo ss uma substituição e {x1,,xm}\{x_{1}, \dots, x_{m}\} um conjunto de variáveis, a restrição de ss ao conjunto de variáveis {x1,,xm}\{x_{1}, \dots, x_{m}\}, escrita s{x1,,xm}={ti/xis:xi{x1,,xm}}.s |_{\{x_{1}, \dots, x_{m}\}} = \{t_{i}/x_{i} \in s : x_{i} \in \{x_{1}, \dots, x_{m}\}\}.

  • Resposta correta de um programa - Uma resposta ss de Δ\Delta ao objetivo α\alpha diz-se correta se Δ(αs)\Delta \models (\alpha \cdot s) (\models lê-se "consequência semântica"). É correta caso Δ{¬αs}\Delta \cup \{\neg\alpha\cdot s\} for contraditório.

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.

Função de Seleção (SS)

Regra para escolher um literal numa cláusula-objetivo como candidato à aplicação do princípio da resolução. É tal que S(α=(α1,,αn))(α1,,αn).S(\leftarrow \alpha = (\alpha_{1}, \dots, \alpha_{n})) \in (\alpha_{1}, \dots, \alpha_{n}).

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 SS uma função de seleção. Se a prova SLD para α\alpha usando Δ\Delta for finita, [γ0,,γn][\gamma_{0}, \dots, \gamma_{n}] (sequência de objetivos), a composição das substituições s0,,sn1s_{0},\dots,s_{n-1} restringida às variáveis que ocorrem em α (s0sn1)vars(α)\alpha~(s_{0} \circ \dots \circ s_{n-1})|_{vars(\alpha)}, diz-se uma resposta calculada de Δ\Delta a α\alpha via SS. Diz-se também que nn é o comprimento da prova SLD.

Exemplo - Resolução SLD

No exemplo seguinte, temos uma resolução SLD, com objetivo Ant(Sr.B,Bart)\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)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:

γ0=Ant(Sr.B,Bart)γ1=Ant(Sr.B,y),AD(y,Bart)γ2=Ant(Sr.B,Marge)γ3=AD(Sr.B,Marge)γ4=\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}{Marge/y}{Sr.B/x,Marge/y}ϵ){}=ϵ(\{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.

Árvore SLD

Sendo Δ\Delta um programa, α\alpha um objetivo e SS uma função de seleção, a árvore SLD de Δ\Delta via SS é uma árvore rotulada, construída do seguinte modo:

  • o rótulo de cada nó é um objetivo;
  • o rótulo da raiz é α\alpha;
  • cada nó com rótulo β1,,βn\leftarrow \beta_{1},\dots,\beta_{n}, tem um ramo por cada cláusula δγ1,,γpΔ\delta \leftarrow \gamma_{1},\dots,\gamma_{p} \in \Delta cuja cabeça é unificável com S(β1,,βn)S(\leftarrow \beta_{1},\dots,\beta_{n}). O rótulo da raiz deste ramo corresponde ao resolvente entre as duas cláusulas.

Numa árvore SLD, os ramos que terminam em \square dizem-se bem sucedidos, sendo que os que terminam em objetivos dizem-se falhados e os restantes ramos infinitos.

Tenhamos o programa:

P(x,z)Q(x,y),P(y,z)P(x,x)Q(a,b)P(x, z) \leftarrow Q(x, y), P(y, z)\\ P(x, x) \leftarrow\\ Q(a, b) \leftarrow\\

e o objetivo:

P(x,b)\leftarrow P(x, b)

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.