Resolução SLD
As refutações por resolução são ‘pesadas’ e ‘caras’, no caso
geral.
Com um conjunto inconsistente de cláusulas existirão,
tipicamente, numerosas formas de derivar a cláusula vazia
através da resolução.
Podem existir muitas formas de escolher as premissas,
enquanto que para cada escolha de premissas podem existir
muitas maneiras de as ‘resolver’ de acordo com os vários
literais disponíveis para um passo da resolução.
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
218
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Resolução SLD
No entanto, em certos fragmentos, podemos definir procedimentos
de refutação eficientes.
É o caso das cláusulas de Horn:
q  p1, ..., pn
 p1, ..., pn
cláusula de programa
objectivo
em que
SLD: D de definidas
Programa é um conjunto (finito) de cláusulas definidas (cláusulas
de programa).
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
219
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Resolução SLD
SLD: L de linear
Cada passo de resolução (aplicação da regra de inferência) usa
como premissa (cláusula central) o resolvente mais recente.
Partindo de um objectivo e um programa, uma derivação (S)LD só
gera objectivos como resolventes.
Prova
Note-se que, em cada passo, sendo a resolução linear, uma das
premissas é um objectivo (o resolvente anterior ou a interrogação inicial)
e que os objectivos só admitem como segunda premissa uma cláusula de
programa. Isto é, num passo de resolução (S)LD a cláusula central é um
objectivo e a outra premissa (cláusula lateral) é uma das cláusulas do
programa. Ora o resolvente de um objectivo e de uma cláusula de
programa é ainda um objectivo.
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
220
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Resolução SLD
SLD: S de selecção
Regra de computação: selecciona, em cada passo, a fórmula
atómica, do objectivo, que vai ser eliminada.
Um objectivo diz-se derivável de um programa P e de um objectivo
G via uma regra de computação S quando é o resolvente de um
passo de resolução, tendo como premissas cP e G, e a fórmula
eliminada é S(G).
Quer dizer, se G for  p1, ..., pk, ..., pm, tal que pk=S(G),
e c for q  q1, ..., qn (o que exige que pk e q sejam unificáveis) o
resolvente é
 (p1, ..., pk-1,q1, ..., qn, pk+1, ..., pm )
em que  é um U.M.G de {pk, q}.
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
221
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Resolução SLD
Uma refutação SLD para P e G0 via S é uma derivação SLD para P
e G0 via S que termina com (derivação bem sucedida).
A resolução mantém a propriedade de ‘refutation complete’ com a
restrição SLD.
Mais do que isso permite a derivação de todas as respostas
distintas à interrogação inicial seja qual for a regra de computação
escolhida. Esta propriedade é conhecida como a independência
da regra de computação.
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
222
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Exemplo
Conside-se a seguinte interrogação e o programa finito
Q1:?avo(amelia, Z)
C1:avo(X,Z)  progenitor(X, Y), progenitor(Y,Z)
C2:progenitor(amelia, jose)
C3:progenitor(jose, luis)
C4:progenitor(jose, miguel)
Construa as árvores em que
a) não utiliza regra de computação
b) selecciona o literal mais à esquerda para efectuar resolução
c) selecciona o literal mais à direita para efectuar resolução
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
223
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Exemplo
Note-se que o primeiro caso é redundante, pois a mesma
resposta é computada mais do que uma vez. As outras duas
árvores utilizam resolução SLD.
Em ambos os casos obtemos o conjunto completo de respostas
possíveis:
{avo(amelia, luis), avo(amelia,miguel)}
de acordo com a independência da regra de computação.
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
224
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Resolução SLD
Uma árvore SLD (computação) para um programa P e um objectivo G via
uma regra de computação S define-se de seguinte modo:
a sua raiz é G
cada nó tem um filho para cada um dos objectivos deriváveis de P via
S (um filho por cada uma das cláusulas do programa cuja cabeça
pode ser unificada com a fórmula do objectivo seleccionada por S).
Assim temos que:
cada ramo da árvore é uma derivação para P e G via S.
um ramo finito com folha (sucesso) indica uma derivação bem
sucedida (refutação).
um ramo finito sem folha indica uma derivação falhada (completa-se
com a folha de insucesso finito).
podem existir ramos infinitos!
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
225
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Resolução SLD
Podemos voltar a enunciar a propriedade de independência da
regra de computação em termos das árvores SLD:
duas árvores SLD para o mesmo programa e objectivo, mas via
regras de computação diferentes, têm o mesmo número de ramos
bem sucedidos e calculam as mesmas respostas.
As árvores
podem ter formas muito distintas, diferindo em
particular nos ramos falhados ou infinitos.
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
226
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Exemplo
Dinastia_1
C1:
C2:
C3:
C4:
ante(X,Z)  pai(X, Y), ante(Y,Z)
ante(X,Z)  pai(X, Z)
pai(joaoII, afonsoV) 
pai(afonsoV, duarte) 
Q1:
ante(joaoII, Q)
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
(quem são os antecessores de joaoII?)
227
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Exemplo (cont.)
Selecção do primeiro
 ante(joaoII, Q)
 pai(joaoII, Y1), ante(Y1, Q)
 pai(joaoII, Q)
 ante(afonsoV, Q)
{Q/afonsoV}
 pai(afonsoV, Y2), ante(Y2, Q)
 ante(duarte, Q)
 pai(duarte, Y3), ante(Y3, Q)
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
 pai(afonsoV, Q)
{Q/duarte}
 pai(duarte, Q)
228
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Exemplo (cont.)
Selecção do último
 ante(joaoII, Q)
 pai(joaoII, Y1), ante(Y1, Q)
 pai(joaoII, Y1), pai(Y1, Y2), ante(Y2, Q)
 pai(joaoII, Q)
 pai(joaoII, Y1), pai(Y1, Q)
{Q/afonsoV}
 pai(joaoII, Y1), pai(Y1, Y2), pai(Y2, Q)
∞
 pai(joaoII, Y1), pai(Y1, joaoII)
 pai(joaoII, joaoII)
 pai(joaoII, afonsoV)
 pai(joaoII, Y1), pai(Y1, afonsoV)
{Q/duarte}
 pai(joaoII, joaoII)
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
229
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Estratégia de Pesquisa
Finalidade:
Determinar a existência de um ramo bem sucedido (refutação).
Possivelmente, determinar todas as respostas calculáveis (uma por
cada ramo bem sucedido).
Questão:
Que estratégia usar para explorar a árvore? (Regra de Pesquisa)
Como construir a árvore?
A necessidade de uma tal estratégia é característica do
formalismos relacionais (existência de mais de uma resposta) em
oposição aos formalismos funcionais.
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
230
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Estratégia de Pesquisa
Execução Sequencial Descendente, em Profundidade, com Retrocesso
Relativamente a cada nó, atribui-se uma prioridade a cada um dos
seus filhos (atribuir uma prioridade a cada uma das cláusulas do
programa cuja cabeça pode ser unificada com a fórmula do objectivo
seleccionada pela regra de computação).
A execução começa com a geração da raiz.
Encontrando-se o controlo num nó, gera-se o filho de maior prioridade
entre os que ainda não foram gerados e passa-se-lhe o controlo.
Se não houver filhos, ou se já tiverem sido todos gerados, então o
controlo é passado ao ascendente mais próximo que ainda tem filhos
por gerar. Se tal ascendente não existe, é porque a árvore já foi
totalmente gerada, terminando-se então a execução.
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
231
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Estratégia de Pesquisa
Esta é a estratégia seguida pelo Prolog, sendo a prioridade
determinada pela ordem das cláusulas no programa - estratégia
padrão.
No nosso exemplo o Prolog teria gerado a primeira árvore (se
seguirmos a convenção habitual de apresentar as computações da
esquerda para a direita ao longo da página de acordo com a ordem
cronológica com que são geradas).
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
232
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Estratégia de Pesquisa
Execução Descendente, em Largura
Todos os nós de uma geração são gerados antes de passar à geração
seguinte (sendo P finito, cada geração é finita).
Se a árvore é finita, a escolha da estratégia de pesquisa é inconsequente
(apenas a ordem das respostas varia).
A pesquisa em profundidade optimiza a utilização de memória. No entanto,
se a árvore possui um ramo infinito, a execução nunca sai desse ramo, e
as respostas calculáveis nos outros ramos não serão geradas
(inadequação).
A pesquisa em largura garante que cada resposta calculável é gerada em
tempo finito (se bem que a pesquisa numa árvore infinita se prolongaria
indefinidamente). No entanto exige demasiada utilização de memória.
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
233
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Regra de Computação e Regra de Pesquisa
PROLOG - Regra de Computação
Escolha do primeiro literal do objectivo.
PROLOG - Regra de Pesquisa
Descendente, em profundidade, escolhendo as cláusulas do
programa de acordo com a ordem pela qual ocorrem no
programa.
Uma vez fixadas, as regras de computação e de pesquisa
permitem escolher, entre programas logicamente equivalentes,
os que têm uma execução mais eficiente fazendo variar a ordem
dos predicados no corpo das cláusulas, e a das cláusulas no
corpo do programa.
É neste sentido que se programa em PROLOG (programação
vs. representação).
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
234
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Regra de Computação e Regra de Pesquisa
A Ordem das Cláusulas determina o percurso de construção.
Pode, por exemplo, comparar-se o percurso de construção da árvore
de pesquisa para o objectivo
ante(joaoII, Q)
e o programa
Dinastia_2
ante(X,Z)  pai(X, Z)
ante(X,Z)  pai(X, Y), ante(Y,Z)
pai(joaoII, afonsoV) 
pai(afonsoV, duarte) 
com o caso anterior (Dinastia_1: ordem inversa das cláusulas para o
procedimento ante)
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
235
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Regra de Computação e Regra de Pesquisa
 ante(joaoII, Q)
 pai(joaoII, Q)
 pai(joaoII, Y1), ante(Y1, Q)
 ante(afonsoV, Q)
{Q/afonsoV}
 pai(afonsoV, Y2), ante(Y2, Q)
 pai(afonsoV, Q)
 ante(duarte, Q)
{Q/duarte}
 pai(duarte, Q)
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
236
 pai(duarte, Y3), ante(Y3, Q)
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Regra de Computação e Regra de Pesquisa
A Ordem dos Predicados determina a forma da árvore.
Pode, por exemplo, comparar-se o percurso de construção da árvore
de pesquisa para o objectivo
ante(joaoII, Q)
e o programa
Dinastia_3
ante(X,Z)  pai(X, Z)
ante(X,Z)  ante(Y,Z), pai(X, Y)
pai(joaoII, afonsoV) 
pai(afonsoV, duarte) 
com o caso anterior (Dinastia_2: ordem inversa dos predicados para a
cláusula recursiva)
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
237
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Regra de Computação e Regra de Pesquisa
 ante(joaoII, Q)
 pai(joaoII, Q)
 ante(Y1, Q), pai(joaoII, Y1)
 ante(Y2, Q), pai(Y1, Y2), pai(joaoII, Y1)
 pai(Y1, Q), pai(joaoII, Y1)
{Q/afonsoV}
 pai(joaoII, joaoII)
 pai(joaoII, afonsoV)
 pai(Y2, Q), pai(Y1, Y2), pai(joaoII, Y1)
 pai(Y1, joaoII), pai(joaoII, Y1)
 pai(Y1, afonsoV), pai(joaoII, Y1)
{Q/duarte}
 pai(joaoII, joaoII)
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
238
∞
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Regra de Computação e Regra de Pesquisa
Que aconteceria se a ordem das cláusulas do procedimento
ante fosse trocada? (Dinastia_4)
Num programa recursivo, a base deve estar antes do passo!
Podemos ainda concluir que a árvore originada por Dinastia_2
é a mais simples (juntamente com Dinastia_1 para este
objectivo). Esta comparação remete-nos para uma regra a
utilizar aquando da resolução de problemas:
é normalmente melhor tentar a ideia mais simples primeiro!
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
239
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Regra de Computação e Regra de Pesquisa
No nosso caso, todas as versões da relação ante(cessor) são
baseadas em 2 ideias:
a ideia mais simples é verificar se os dois argumentos da
relação satisfazem a relação de pai.
a ideia mais complicada é descobrir alguém entre as
duas pessoas (alguém que esteja relacionado com elas
através da relação de pai e antecessor)
No caso de Dinastia_2 as ideias mais simples são resolvidas
em primeiro lugar.
No caso de Dinastia_4 tenta-se sempre resolver as ideias mais
complicadas em primeiro lugar.
Universidade da Madeira
Departamento de Matemática
Elsa Carvalho
240
Programação em Lógica e Funcional (2000/01)
(Actualizado em 2004/05)
Download

11 - Universidade da Madeira