Resolução SLD - SLD resolution

A resolução SLD ( resolução de cláusula seletiva linear definida ) é a regra básica de inferência usada na programação lógica . É um refinamento da resolução , que é tanto som e refutação completa de cláusulas de Horn .

A regra de inferência SLD

Dada uma cláusula objetivo, representada como a negação de um problema a ser resolvido:

${\ displaystyle \ neg L_ {1} \ lor \ cdots \ lor \ neg L_ {i} \ lor \ cdots \ lor \ neg L_ {n}}$

com literal selecionado e uma cláusula definida de entrada : ${\ displaystyle \ neg L_ {i}}$

${\ displaystyle L \ lor \ neg K_ {1} \ lor \ cdots \ lor \ neg K_ {m}}$

cujo literal positivo (átomo) unifica-se com o átomo do literal selecionado , a resolução SLD deriva outra cláusula objetivo, em que o literal selecionado é substituído pelos literais negativos da cláusula de entrada e a substituição unificadora é aplicada: ${\ displaystyle L \,}$ ${\ displaystyle L_ {i} \,}$${\ displaystyle \ neg L_ {i} \,}$${\ displaystyle \ theta \,}$

${\ displaystyle (\ neg L_ {1} \ lor \ cdots \ lor \ neg K_ {1} \ lor \ cdots \ lor \ neg K_ {m} \ \ lor \ cdots \ lor \ neg L_ {n}) \ theta }$

No caso mais simples, na lógica proposicional, os átomos e são idênticos, e a substituição unificadora é vazia. No entanto, no caso mais geral, a substituição unificadora é necessária para tornar os dois literais idênticos. ${\ displaystyle L_ {i} \,}$${\ displaystyle L \,}$${\ displaystyle \ theta \,}$

A origem do nome "SLD"

O nome "resolução SLD" foi dado por Maarten van Emden para a regra de inferência não nomeada introduzida por Robert Kowalski . Seu nome é derivado da resolução do SL, que é ao mesmo tempo sólida e refutação completa para a forma oracional irrestrita da lógica. "SLD" significa "Resolução de SL com cláusulas definidas".

Em ambos, SL e SLD, "L" representa o fato de que uma prova de resolução pode ser restrita a uma sequência linear de cláusulas:

${\ displaystyle C_ {1}, C_ {2}, \ cdots, C_ {l}}$

onde a "cláusula principal" é uma cláusula de entrada e todas as outras cláusulas são resolventes, uma de cujos pais é a cláusula anterior . A prova é uma refutação se a última cláusula for a cláusula vazia. ${\ displaystyle C_ {1} \,}$${\ displaystyle C_ {i + 1} \,}$${\ displaystyle C_ {i} \,}$${\ displaystyle C_ {l} \,}$

Em SLD, todas as cláusulas na sequência são cláusulas de objetivo e o outro pai é uma cláusula de entrada. Na resolução do SL, o outro pai é uma cláusula de entrada ou uma cláusula ancestral anterior na sequência.

Em ambos SL e SLD, "S" representa o fato de que o único literal resolvido em qualquer cláusula é aquele que é exclusivamente selecionado por uma regra de seleção ou função de seleção. Na resolução SL, o literal selecionado é restrito a um que foi introduzido mais recentemente na cláusula. No caso mais simples, essa função de seleção do último a entrar, primeiro a sair pode ser especificada pela ordem em que os literais são escritos, como em Prolog . No entanto, a função de seleção na resolução SLD é mais geral do que na resolução SL e no Prolog. Não há restrição quanto ao literal que pode ser selecionado. ${\ displaystyle C_ {i} \,}$

A interpretação computacional da resolução SLD

Na lógica das orações, uma refutação do SLD demonstra que o conjunto de cláusulas de entrada é insatisfatório. Na programação lógica, no entanto, uma refutação SLD também tem uma interpretação computacional. A cláusula superior pode ser interpretada como a negação de uma conjunção de subobjetivos . A derivação da cláusula de é a derivação, por meio do raciocínio retroativo , de um novo conjunto de sub-objetivos usando uma cláusula de entrada como um procedimento de redução do objetivo. A substituição unificadora passa a entrada da subobjetiva selecionada para o corpo do procedimento e simultaneamente passa a saída da cabeça do procedimento para as subobjetivas não selecionadas restantes. A cláusula vazia é simplesmente um conjunto vazio de submetas, o que sinaliza que a conjunção inicial de submetas na cláusula superior foi resolvida. ${\ displaystyle \ neg L_ {1} \ lor \ cdots \ lor \ neg L_ {i} \ lor \ cdots \ lor \ neg L_ {n}}$${\ displaystyle L_ {1} \ land \ cdots \ land L_ {i} \ land \ cdots \ land L_ {n}}$${\ displaystyle C_ {i + 1} \,}$${\ displaystyle C_ {i} \,}$${\ displaystyle \ theta \,}$

Estratégias de resolução SLD

A resolução SLD define implicitamente uma árvore de pesquisa de cálculos alternativos, na qual a cláusula de objetivo inicial está associada à raiz da árvore. Para cada nó na árvore e para cada cláusula definida no programa cujo literal positivo se une ao literal selecionado na cláusula goal associada ao nó, há um nó filho associado à cláusula goal obtida pela resolução SLD.

Um nó folha, que não tem filhos, é um nó de sucesso se sua cláusula de objetivo associada for a cláusula vazia. É um nó de falha se sua cláusula de objetivo associada não estiver vazia, mas seu literal selecionado se unificar com nenhum literal positivo de cláusulas definidas no programa.

A resolução SLD é não determinística no sentido de que não determina a estratégia de busca para explorar a árvore de busca. O Prolog pesquisa a profundidade da árvore primeiro, um ramo de cada vez, usando retrocesso quando encontra um nó de falha. A pesquisa em profundidade é muito eficiente no uso de recursos de computação, mas é incompleta se o espaço de pesquisa contém ramificações infinitas e a estratégia de pesquisa procura essas ramificações em vez de ramificações finitas: o cálculo não termina. Outras estratégias de pesquisa, incluindo pesquisa abrangente , melhor primeiro e ramificada também são possíveis. Além disso, a busca pode ser realizada sequencialmente, um nó por vez, ou em paralelo, vários nós simultaneamente.

A resolução SLD também é não determinística no sentido, mencionado anteriormente, de que a regra de seleção não é determinada pela regra de inferência, mas é determinada por um procedimento de decisão separado, que pode ser sensível à dinâmica do processo de execução do programa.

O espaço de busca de resolução SLD é uma árvore or, na qual diferentes ramos representam cálculos alternativos. No caso de programas de lógica proposicional, o SLD pode ser generalizado de forma que o espaço de busca seja uma árvore and-or , cujos nós são rotulados por literais únicos, representando subobjetivos, e os nós são unidos por conjunção ou disjunção. No caso geral, onde as submetas conjuntas compartilham variáveis, a representação da árvore e / ou é mais complicada.

Exemplo

Dado o programa lógico:

q :- p.
p.

e a meta de nível superior:

q.

o espaço de busca consiste em um único ramo, no qual q é reduzido ao p qual é reduzido ao conjunto vazio de submetas, sinalizando um cálculo bem-sucedido. Nesse caso, o programa é tão simples que não há função para a função de seleção e não há necessidade de nenhuma pesquisa.

Na lógica oracional, o programa é representado pelo conjunto de cláusulas:

${\ displaystyle q \ lor \ neg p}$

${\ displaystyle p \,}$

e a meta de nível superior é representada pela cláusula da meta com um único literal negativo:

${\ displaystyle \ neg q}$

O espaço de busca consiste na única refutação:

${\ displaystyle \ neg q, \ neg p, {\ mathit {false}}}$

onde representa a cláusula vazia. ${\ displaystyle {\ mathit {false}} \,}$

Se a seguinte cláusula foi adicionada ao programa:

q :- r.

então haveria uma ramificação adicional no espaço de pesquisa, cujo nó folha r é um nó de falha. No Prolog, se esta cláusula fosse adicionada à frente do programa original, então o Prolog usaria a ordem em que as cláusulas são escritas para determinar a ordem em que as ramificações do espaço de busca são investigadas. O Prolog tentaria primeiro esse novo branch, falharia e então voltaria para investigar o único branch do programa original e teria sucesso.

Se a cláusula

p :- p.

foram adicionados ao programa, a árvore de pesquisa conteria um ramo infinito. Se essa cláusula fosse tentada primeiro, o Prolog entraria em um loop infinito e não encontraria o desvio bem-sucedido.

SLDNF

SLDNF é uma extensão da resolução SLD para lidar com a negação como falha . Em SLDNF, as cláusulas de objetivo podem conter negação como literais de falha, digamos do formulário , que pode ser selecionado apenas se não contiverem variáveis. Quando tal literal livre de variável é selecionado, uma subprova (ou subcomputação) é tentada para determinar se há uma refutação SLDNF começando do literal não negado correspondente como cláusula superior. A submeta selecionada é bem-sucedida se a subprova falhar, e falha se a subprova for bem-sucedida. ${\ displaystyle not (p) \,}$${\ displaystyle p \,}$${\ displaystyle not (p) \,}$

Veja também

• John Alan Robinson

Referências

• Jean Gallier , SLD-Resolution and Logic Programming, capítulo 9 de Logic for Computer Science: Foundations of Automatic Theorem Proving , revisão online de 2003 (download gratuito), publicado originalmente por Wiley, 1986
• John C. Shepherdson, SLDNF-Resolution with Equality , Journal of Automated Reasoning 8: 297-306, 1992; define a semântica em relação a qual resolução SLDNF com igualdade é sólida e completa

links externos

• [1] Definição do Dicionário Online Livre de Computação