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.