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 p
falhar, então afirme ¬p
. Isso afirma que a proposição p
deve 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
- K. Clark [1978, 1987]. Negação como falha . Leituras em raciocínio não monotônico , Morgan Kaufmann Publishers, páginas 311-325.
- M. Gelfond [1987] On Stratified Autoepistemic Theories Proc. AAAI 1987, páginas 207-211.
- M. Gelfond e V. Lifschitz [1988] The Stable Model Semantics for Logic Programming Proc. 5th International Conference and Symposium on Logic Programming (R. Kowalski e K. Bowen, eds), MIT Press, páginas 1070-1080.
- JC Shepherdson [1984] Negation as Failure: A Comparison of Clark's Completed Data Dase e Reiter's Closed World Assumption , Journal of Logic Programming, vol 1, 1984, páginas 51-81.
- JC Shepherdson [1985] Negation as Failure II , Journal of Logic Programming, vol 3, 1985, páginas 185-202.
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).