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 ${\displaystyle \mathrm {not} ~p}$ (isto é, ${\displaystyle p}$ não se verifica) da falha em derivar ${\displaystyle p}$. Note que ${\displaystyle \mathrm {not} ~p}$ pode ser diferente do enunciado ${\displaystyle \neg p}$ (negação lógica de ${\displaystyle 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^[1]. 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 ${\displaystyle 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:

${\displaystyle p\leftarrow q\land \mathrm {not} ~r}$

${\displaystyle q\leftarrow s}$

${\displaystyle q\leftarrow t}$

${\displaystyle t\leftarrow }$

Negação por falha deriva ${\displaystyle \mathrm {not} ~s}$, ${\displaystyle \mathrm {not} ~r}$ e ${\displaystyle ~p}$.

Semântica de Completação

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 ${\displaystyle \leftarrow }$ são interpretados como "se e somente se", escritos como "sse" ou "${\displaystyle \equiv }$".

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

${\displaystyle p\equiv q\land \mathrm {not} ~r}$

${\displaystyle q\equiv s\lor t}$

${\displaystyle t\equiv \mathrm {true} }$

${\displaystyle r\equiv \mathrm {false} }$

${\displaystyle 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 ${\displaystyle \mathrm {not} ~p}$, Negação por Falha simula raciocínio com as equivalências

${\displaystyle \mathrm {not} ~p\equiv \mathrm {not} ~q\lor r}$

${\displaystyle \mathrm {not} ~q\equiv \mathrm {not} ~s\land \mathrm {not} ~t}$

${\displaystyle \mathrm {not} ~t\equiv \mathrm {false} }$

${\displaystyle \mathrm {not} ~r\equiv \mathrm {true} }$

${\displaystyle \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:

${\displaystyle p(a)\leftarrow }$

${\displaystyle p(b)\leftarrow t}$

Negação por Falha deriva ${\displaystyle \mathrm {not} ~p(c)}$.

A Completação do programa é:

${\displaystyle 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.

Referências