# Lógica, unificação e execução em Prolog

Cláusulas de Horn, unificação passo a passo, resolução SLD e negação por falha.

Página: https://resumos.rgo.pt/cadeiras/pfl/logica-unificacao-prolog/

Em Prolog não escreves como calcular. Declaras **factos** (o que é verdade) e **regras** (o que se conclui), fazes uma **query**, e o motor procura a resposta por ti. O programa é uma base de conhecimento; a execução é procura com retrocesso. A lógica por baixo é a [lógica proposicional e de predicados](https://resumos.rgo.pt/cadeiras/md/logica-proposicional/) de MD, restrita a **cláusulas de Horn**: no máximo um literal positivo, o que torna a procura tratável.

## Factos, regras e queries

```
pai(tomas, ana).
pai(ana, leo).
pai(leo, rui).
avo(X, Z) :- pai(X, Y), pai(Y, Z).
```

As três primeiras linhas são factos: Tomás é pai da Ana, e por aí fora. A última é uma regra, lida “X é avô de Z **se** X é pai de Y **e** Y é pai de Z”. As maiúsculas são **variáveis** (por preencher); as minúsculas são **átomos** (valores concretos). A query `?- avo(ana, X).` pede os X que satisfazem a relação, e o Prolog responde `X = rui`.

## Unificação

Antes de procurar, o motor precisa de casar termos. **Unificar** dois termos é encontrar a substituição mínima de variáveis que os torna iguais:

*   `pai(ana, X)` com `pai(ana, leo)` unifica com `{X/leo}`.
*   `pai(X, leo)` com `pai(ana, leo)` unifica com `{X/ana}`.
*   `pai(X, leo)` com `pai(tomas, ana)` falha: `leo` nunca iguala `ana`, e nenhuma substituição muda átomos.

A substituição aplica-se a toda a query de uma vez, o que propaga cada descoberta a todos os lugares onde a variável aparece. É este mecanismo, e não atribuição, que move valores pelo programa.

O diagrama emparelha os dois primeiros exemplos com os factos: à esquerda a query, à direita o facto, e no meio a substituição que os iguala. O terceiro par não tem seta de sucesso porque nenhum facto casa `tomas` com `ana` na segunda posição.

![Unificação de pai(ana, X) com pai(ana, leo) pela substituição X igual a leo; pai(X, leo) com pai(tomas, ana) falha.](https://resumos.rgo.pt/cadeiras/pfl/logica-unificacao-prolog/figura-1.svg)

## Resolução SLD passo a passo

Para responder `?- avo(ana, X).`, o motor constrói uma **árvore de procura**. Segue o ramo de sucesso:

1.  A query unifica com a cabeça da regra `avo(X', Z')`, com `{X'/ana, Z'/X}`. Restam os subobjetivos `pai(ana, Y), pai(Y, X)`.
2.  `pai(ana, Y)` unifica com o facto `pai(ana, leo)`: `{Y/leo}`. Resta `pai(leo, X)`.
3.  `pai(leo, X)` unifica com `pai(leo, rui)`: `{X/rui}`. Não resta nada: sucesso, e a resposta compõe as substituições, `X = rui`.

Se pedires mais soluções (`;`), o motor faz **retrocesso**: volta ao último ponto com alternativas por explorar. Aqui não há mais factos `pai(ana, _)` nem `pai(leo, _)`, por isso responde `false`. Desenhar esta árvore é a técnica de estudo da página: quando o programa diz `false` onde esperavas resposta, o desenho mostra o ramo que morreu e a cláusula em falta.

A árvore completa da query, com o ramo de sucesso e o beco do retrocesso:

![Árvore SLD de avo(ana, X): a query unifica com a regra, pai(ana, Y) casa com o facto dando Y igual a leo, pai(leo, X) casa dando X igual a rui; o retrocesso não encontra alternativas.](https://resumos.rgo.pt/cadeiras/pfl/logica-unificacao-prolog/figura-2.svg)

Corre a query no navegador com os factos da página:

```prolog
pai(tomas, ana).
pai(ana, leo).
pai(leo, rui).
avo(X, Z) :- pai(X, Y), pai(Y, Z).

main :- avo(ana, X), writeln(X).
```

Carrega em **Executar**: imprime `rui`, a mesma resposta construída à mão na árvore.

## Negação por falha

`\+ Objetivo` sucede quando o objetivo **não se prova**:

```
?- \+ pai(rui, _).
true.
```

Não há facto com `rui` como pai, a prova falha finitamente, e a negação sucede. Isto é “negação por falha”, não negação lógica: o motor não prova que é falso, constata que não consegue provar que é verdade.

Variáveis livres na negação

`?- \+ pai(X, leo).` responde `false`, e não “ninguém”. Como `pai(ana, leo)` prova-se com `X = ana`, a negação falha, e o `X` fica por ligar. Regra prática: só nega objetivos sem variáveis por preencher, ou liga-as antes. Este é o erro mais traiçoeiro dos primeiros programas.

## Para saber mais

[Vídeo: Começar em Prolog (curso em português)](https://www.youtube.com/watch?v=ycHLj12bm0M)

A miniatura vem do YouTube. O vídeo só carrega quando clicas. [Abrir no YouTube](https://www.youtube.com/watch?v=ycHLj12bm0M)

*   [SWISH](https://swish.swi-prolog.org/): corre Prolog no navegador, com tutoriais embutidos para experimentar as queries destas páginas.
*   [Learn Prolog Now, capítulo 2](https://lpn.swi-prolog.org/lpnpage.php?pageid=lpn-htmlch2&pagetype=html): unificação passo a passo, com exercícios.
*   [Unificação no Wikibooks](https://pt.wikibooks.org/wiki/Prolog/Unifica%C3%A7%C3%A3o): a mesma matéria explicada em português, com exemplos.