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

Termos, factos e regras

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

• Um facto declara um caso conhecido. A regra diz que X é avô de Z se existir um Y com ambas as relações pai. A vírgula é conjunção.
• Maiúsculas iniciam variáveis; minúsculas iniciam átomos. Cada _ é uma variável anónima nova.
• Um termo é uma variável, uma constante ou uma estrutura. Functor e aridade têm de coincidir: pessoa(ana) não unifica com pessoa(ana,20).
• Um termo sem variáveis é ground. O universo de Herbrand reúne os termos ground construídos com os símbolos do programa.
• Uma cláusula de Horn tem no máximo um literal positivo; uma definida tem exatamente um, a cabeça. H :- A,B corresponde a H ∨ ¬A ∨ ¬B.

Unificar e renomear

Unificar é obter a substituição que torna dois termos iguais, procurando a mais geral. As ligações propagam-se a todas as ocorrências da variável.

Termos	Resultado
par(X,f(X)) e par(a,Y)	X=a, Y=f(a): propaga a primeira ligação.
par(X,X) e par(a,b)	Falha: a primeira ligação exigiria a=b.
par(_,_) e par(a,b)	Sucesso: as anónimas são independentes.

• Antes de cada resolução, renomeia as variáveis da cláusula copiada: duas utilizações da mesma regra não podem partilhar variáveis.
• Em termos finitos de Herbrand, X=f(X) falha pelo occurs check. O =/2 de SWI-Prolog aceita em geral árvores racionais cíclicas; unify_with_occurs_check/2 rejeita a criação desse ciclo. Não confundas o contrato da implementação com a teoria.

Resolução SLD e retrocesso

1. Copia a cláusula com variáveis frescas.
2. Unifica a cabeça com o objetivo escolhido e substitui-o pelo corpo.
3. Propaga as substituições aos objetivos restantes. Lista de objetivos vazia significa sucesso.
4. Ao falhar ou pedir mais respostas, retrocede ao último ponto com alternativas e desfaz as ligações desse ramo.

Prolog escolhe normalmente o objetivo mais à esquerda, tenta cláusulas de cima para baixo e explora em profundidade. Com p :- p. antes de p., um ramo infinito impede chegar ao facto; trocar as cláusulas permite uma primeira resposta, mas pedir todas volta ao ramo infinito.

Quando o programa diz false onde esperavas resposta, desenha a árvore: ela mostra o ramo que morreu e a cláusula em falta.

Negação por falha

\+ G sucede se a tentativa de provar G falhar finitamente. Se G divergir, a negação também não termina; ausência de prova não é prova lógica de falsidade.

• Com pai(ana,leo), \+ pai(X,leo) falha porque existe uma prova; não enumera quem não é pai. Gera e liga candidatos antes de negar.
• O resultado depende da base disponível e pode mudar ao acrescentar factos.

Traços de resolução.