Negação como falha - Negation as failure

Negação como falha ( NAF , para abreviar) é uma regra de inferência não monotônica na programação lógica , usada para derivar (isto é, presume-se que não seja válida) da falha de derivar . Observe que pode ser diferente da declaração da negação lógica de , dependendo da integridade do algoritmo de inferência e, portanto, também do sistema lógico formal.

A negação como falha tem sido um recurso importante da programação lógica desde os primeiros dias do Planner e do Prolog . No Prolog, é geralmente implementado usando construções extralógicas do Prolog.

De maneira mais geral, esse tipo de negação é conhecido como negação fraca , em contraste com a negação forte (ou seja, explícita, demonstrável).

Semântica do planejador

No Planner, a negação como falha pode ser implementada da seguinte forma:

if (not (goal p)), then (assert ¬p)

que diz que se uma busca exaustiva para provar pfalhar, então afirme ¬p. Isso afirma que a proposição pdeve ser assumida como "não verdadeira" em qualquer processamento subsequente. No entanto, como o Planner não é baseado em um modelo lógico, uma interpretação lógica do precedente permanece obscura.

Semântica Prolog

No Prolog puro, os literais NAF da forma podem ocorrer no corpo das cláusulas e podem ser usados ​​para derivar outros literais NAF. Por exemplo, dadas apenas as quatro cláusulas

NAF deriva , e , bem como e .

Semântica de conclusão

A semântica do NAF permaneceu uma questão em aberto até 1978, quando Keith Clark mostrou que é correta com relação à conclusão do programa lógico, onde, falando vagamente, "apenas" e são interpretados como "se e somente se", escrito como "iff" ou " ".

Por exemplo, o preenchimento das quatro cláusulas acima é

A regra de inferência NAF simula o raciocínio explicitamente com a conclusão, onde ambos os lados da equivalência são negados e a negação do lado direito é distribuída para fórmulas atômicas . Por exemplo, para mostrar , o NAF simula o raciocínio com as equivalências

No caso não proposicional, a conclusão precisa ser aumentada com axiomas de igualdade, para formalizar a suposição de que indivíduos com nomes distintos são distintos. NAF simula isso por falha de unificação. Por exemplo, dadas apenas as duas cláusulas

t

NAF deriva .

A conclusão do programa é

aumentado com axiomas de nomes exclusivos e axiomas de encerramento de domínio.

A semântica de conclusão está intimamente relacionada à circunscrição e à suposição de mundo fechado .

Semântica autoepistêmica

A semântica de conclusão justifica interpretar o resultado de uma inferência NAF como a negação clássica de . Porém, em 1987, Michael Gelfond mostrou que também é possível interpretar literalmente como " não pode ser mostrado", " não se sabe" ou " não se acredita", como na lógica autoepistêmica . A interpretação autoepistêmica foi desenvolvida posteriormente por Gelfond e Lifschitz em 1988 e é a base da programação do conjunto de respostas .

A semântica autoepistêmica de um programa Prolog puro P com literais NAF é obtida pela "expansão" P com um conjunto de literais NAF básicos (livres de variável) Δ que é estável no sentido de que

Δ = { | não está implícito em P ∪ Δ}

Em outras palavras, um conjunto de suposições Δ sobre o que não pode ser mostrado é estável se e somente se Δ for o conjunto de todas as sentenças que realmente não podem ser mostradas a partir do programa P expandido por Δ. Aqui, por causa da sintaxe simples dos programas Prolog puros, "implícito por" pode ser entendido muito simplesmente como derivabilidade usando modus ponens e instanciação universal sozinha.

Um programa pode ter zero, uma ou mais expansões estáveis. Por exemplo,

não tem expansões estáveis.

tem exatamente uma expansão estável Δ = { }

tem exatamente duas expansões estáveis ​​Δ 1 = { } e Δ 2 = { }.

A interpretação autoepistêmica do NAF pode ser combinada com a negação clássica, como na programação lógica estendida e na programação do conjunto de respostas . Combinando as duas negações, é possível expressar, por exemplo

(a suposição do mundo fechado) e
( mantém por padrão).

Notas de rodapé

Referências

links externos

  • Relatório do Workshop do W3C sobre Linguagens de Regras para Interoperabilidade. Inclui notas sobre NAF e SNAF (negação com escopo como falha).