Negação por falha

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

Negação por falha, é uma regra de inferência não-monotônica na programação em lógica, usada para derivar (isto é, não se verifica) da falha em derivar . Note que pode ser diferente do enunciado (negação lógica de ), dependendo da completude do algoritmo de inferência e assim, também do sistema lógico formal.

Negação por falha é uma importante caracterísitca da programação em lógica desde seu uso inicial em linguagens de programação como Planner e Prolog. Em Prolog, é normalmente implementada usando os construtos extralógicos do Prolog.

Lógica[editar | editar código-fonte]

Em lógica, a interpretação padronizada da negação é que a negação de uma fórmula é verdadeira se e somente se a fórmula é falsa. Se uma fórmula não é nem verdadeira nem falsa, sua negação é considerada desconhecida. Na interpretação da negação por falha, a negação da fórmula nesse caso é considerada verdadeira.

A negação por falha é relacionada com a suposição comum de que o que não é conhecido ser verdadeiro é falso. Isso é conhecido como a Hipótese do Mundo Fechado (Closed-World Assumption).

Em argumentação, um ponto para o qual nenhum argumento pode ser feito é chamado um argumento infundado. Um argumento infundado para α não é um argumento fundado para a negação de α.

Semântica em Planner[editar | editar código-fonte]

Em Planner, negação por falha pode ser implementada da seguinte maneira:

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

que significa que se uma busca exaustiva para provar p falhar, então assuma ¬p[1]. Note que o exemplo acima efetivamente utiliza notação matemática, que não pode ser representada em Prolog.

Semântica em Prolog[editar | editar código-fonte]

Em Prolog puro, literais de Negação por Falha na forma podem ocorrer no corpo de cláusulas e podem ser usados para derivar outros literais de Negação por Falha. Por exemplo, dada apenas quatro cláusulas:

Negação por falha deriva , e .

Semântica de Completação[editar | editar código-fonte]

As semânticas de Negação por Falha permaneceram uma questão em aberto até que Keith Clark[2] mostrou que é correto, em relação à completação do programa lógico, onde, vagamente falando, "apenas" e são interpretados como "se e somente se", escritos como "sse" ou "".

Por exemplo, a completação das quatro cláusulas anteriormente citadas é:

A regra de inferência de Negação por Falha simula raciocínio explicitamente com a completação, nos quais ambos os lados da equivalência são negados e a negação do lado direito é distribuída até a fórmula atômica. Por exemplo, para demonstrar , Negação por Falha simula raciocínio com as equivalências

No caso não-proposicional, a completação precisa ser ampliada com axiomas de igualdade, para formalizar a hipótese de que indivíduos com nomes distintos são distintos. Negação por Falha simula isso através da falha de unificação. Por exemplo, dadas apenas duas cláusulas:

Negação por Falha deriva .

A Completação do programa é:

aumentada com axiomas de nome único e axiomas de fecho de domínio.

A semântica de completação é fortemente relacionada à circunscrição e à Hipótese do Mundo Fechado.

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

  1. Clark, Keith (1978). Logic and Data Bases (PDF) Springer-Verlag [S.l.] p. 293–322. ISBN 10.1007/978-1-4684-3384-5_11 Verifique |isbn= (Ajuda). 
  2. Clark, Keith. Negation as failure. Readings in nonmonotonic reasoning Morgan Kaufmann Publishers [S.l.] p. 311-325.