Resolução SLD

Resolução SLD (resolução Seletiva Linear para cláusula definida), é a regra de inferência básica usada em lógica de programação. É um refinamento do principio da resolução, que é correta e completa para cláusulas de Horn.

A regra de inferência SLD

De uma determinada cláusula:

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

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

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

cujo literal positivo (atom) $L\,$ unifica com o atômico $L_{i}\,$ do literal selecionado  $\neg L_{i}\,$, resolução SLD deriva outra  cláusula, no qual o literal selecionado é substituído pelos literais negativos de entrada  da cláusula e o unificador de substituição $\theta \,$ é aplicado:

$(\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, em lógica proposicional, os atômicos $L_{i}\,$ e $L\,$ são idênticos, e a substituição unificadora $\theta \,$ é vazia. No entanto, no caso mais geral, a a substituição unificadora é necessária para tornar os dois literais idênticos.

A origem do nome "SLD"

O nome "resolução SLD" foi dado por Maarten van Emden para a regra de inferência  sem nome introduzida por Robert Kowalski. Seu nome é derivado da resolução SL , que é correta e completa para a forma de lógica clausal irrestrita. "SLD" significa "SL resolution with Definite clauses".

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

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

onde a "top clause" $C_{1}\,$ é uma cláusula de entrada, e cada cláusula $C_{i+1}\,$ é uma resolvente, um dos progenitores é a cláusula anterior $C_{i}\,$. A prova é uma refutação, se a última cláusula $C_{l}\,$ é a cláusula vazia.

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

Em ambos SL e SLD, "S" significa o fato de que o único literal resolvido em qualquer cláusula $C_{i}\,$ é 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 tenha sido mais recentemente introduzido na cláusula. No caso mais simples, como uma função de seleção "last-in-first-out" podem ser especificados 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 em Prolog. Não há nenhuma restrição no literal, que pode ser selecionado.

Estratégias de resolução

A resolução SLD define implicitamente uma árvore de busca de alternativas de cálculos, em que a cláusula inicial está associada com a raiz da árvore. Para cada nó da árvore e para cada cláusula definida no programa cujo literal positivo unifica com o literal da cláusula associada com o nó,existe um nó filho associado com o da cláusula obtido pela resolução SLD.

A resolução SLD é não-determinística no sentido de que não é possível determinar a estratégia de busca para explorar a árvore de busca. A linguagem de programação Prolog realiza a busca em profundidade (DFS), um ramo de cada vez, usando  backtracking quando encontra um  nó falho (cláusula associada não vazia). A busca em profundidade é muito eficiente no uso de recursos de computação, mas é incompleta se o espaço de busca contém infinitos ramos e a estratégia de pesquisa procura estes de preferência para finitos ramos: o processamento nunca termina. Outras estratégias de pesquisa, incluindo busca  em largura, melhor-em primeiro lugar, e "branch-and-bound search" também são possíveis. Além disso, a pesquisa pode ser realizada de forma sequencial, um nó de cada vez, ou em paralelo, vários nós simultaneamente.

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

Exemplo

Dado o programa lógico:

q :- p

p

e o objetivo:

q

o espaço de busca consiste em um único ramo, no qual q é reduzido para p , que é reduzido ao conjunto vazio, o que comprova o sucesso de um cálculo. Neste caso, o programa é tão simples que não há função para a função de seleção e sem necessidade de qualquer pesquisa.

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

$q\lor \neg p$

$p\,$

e o objetivo é representado pelo objetivo de cláusula com um único literal negativo:

$\neg q$

O espaço de busca é composto de uma única refutação:

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

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

SLDNF

SLDNF é uma extensão da resolução SLD para lidar com a negação por falha. Em SLDNF, as cláusulas podem conter negação por falha como literais, a dizer da forma $not(p)\,$, que pode ser selecionado somente se elas não contêm variáveis. Quando uma variável livre literal é selecionada, uma subproof (ou subcomputation) tentativa para determinar se há um SLDNF refutação partir da correspondente não-negado $p\,$ como cláusula top. O literal selecionado  $not(p)\,$  é um êxito se o subproof falha, e falha se o subproof tem êxito.

Ver também

• John Alan Robinson

Ligações externas

• Definitionfrom the Free On-Line Dictionary of Computing