Resolução SLD

Origem: Wikipédia, a enciclopédia livre.

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 é corretacompleta para cláusulas de Horn.


A regra de inferência SLD[editar | editar código-fonte]

De uma determinada cláusula:

com o literal  selecionado, e uma cláusula de entrada definida :

cujo literal positivo (atom) unifica com o atômico  do literal selecionado  , 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 é aplicado:

No caso mais simples, em lógica proposicional, os atômicos  e são idênticos, e a substituição unificadora é 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"[editar | editar código-fonte]

O nome "resolução SLD" foi dado por Maarten van Emden para a regra de inferência  sem nome introduzida por Robert Kowalski.[1] Seu nome é derivado da resolução SL [2], 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:

onde a "top clause" é uma cláusula de entrada, e cada cláusula é uma resolvente, um dos progenitores é a cláusula anterior . A prova é uma refutação, se a última cláusula é 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 é 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[editar | editar código-fonte]

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[editar | editar código-fonte]

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:

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

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

onde representa a cláusula vazia.

SLDNF[editar | editar código-fonte]

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 , 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 como cláusula top. O literal selecionado    é um êxito se o subproof falha, e falha se o subproof tem êxito.

Veja também[editar | editar código-fonte]

Referências[editar | editar código-fonte]

  1. Robert Kowalski Predicate Logic as a Programming Language Memo 70, Department of Artificial Intelligence, Edinburgh University. 1973.
  2. Robert Kowalski and Donald Kuehner, Linear Resolution with Selection Function Artificial Intelligence, Vol. 2, 1971, pp. 227-60.

links externos[editar | editar código-fonte]

  • [1] Definition from the Free On-Line Dictionary of Computing