# 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.