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  \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[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 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 \and \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[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 \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 \and \mathrm{not}~r

q \equiv s \or 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 \or r

\mathrm{not}~q \equiv \mathrm{not}~s \and \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 \or 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[editar | editar código-fonte]

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