# Negação por falha

Negação por falha, é uma regra de inferência não-monotônica na programação em lógica, usada para derivar $\mathrm {not} ~p$ (isto é, $p$ não se verifica) da falha em derivar $p$. Note que $\mathrm {not} ~p$ pode ser diferente do enunciado $\neg p$ (negação lógica de $p$), 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

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

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. Note que o exemplo acima efetivamente utiliza notação matemática, que não pode ser representada em Prolog.

## Semântica em Prolog

Em Prolog puro, literais de Negação por Falha na forma $not~p$ 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:
$p\leftarrow q\land \mathrm {not} ~r$
$q\leftarrow s$
$q\leftarrow t$
$t\leftarrow$
Negação por falha deriva $\mathrm {not} ~s$, $\mathrm {not} ~r$ e $~p$.

## Semântica de Completação

As semânticas de Negação por Falha permaneceram uma questão em aberto até que Keith Clark mostrou que é correto, em relação à completação do programa lógico, onde, vagamente falando, "apenas" e $\leftarrow$ são interpretados como "se e somente se", escritos como "sse" ou "$\equiv$".
Por exemplo, a completação das quatro cláusulas anteriormente citadas é:
$p\equiv q\land \mathrm {not} ~r$
$q\equiv s\lor t$
$t\equiv \mathrm {true}$
$r\equiv \mathrm {false}$
$s\equiv \mathrm {false}$
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 $\mathrm {not} ~p$, Negação por Falha simula raciocínio com as equivalências
$\mathrm {not} ~p\equiv \mathrm {not} ~q\lor r$
$\mathrm {not} ~q\equiv \mathrm {not} ~s\land \mathrm {not} ~t$
$\mathrm {not} ~t\equiv \mathrm {false}$
$\mathrm {not} ~r\equiv \mathrm {true}$
$\mathrm {not} ~s\equiv \mathrm {true}$
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:
$p(a)\leftarrow$
$p(b)\leftarrow t$
Negação por Falha deriva $\mathrm {not} ~p(c)$.
A Completação do programa é:
$p(X)\equiv X=a\lor X=b$
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.