negation by failure

Negation as failure

Negation as failure (NAF, for short) is a non-monotonic inference rule in logic programming, used to derive not~p from failure to derive p. It has been an important feature of logic programming since the earliest days of both Planner and Prolog. In Prolog, it is usually implemented using Prolog's extralogical constructs.

In pure Prolog, NAF literals of the form not~p can occur in the body of clauses and can be used to derive other NAF literals. For example, given only the four clauses

p leftarrow q and not~r
q leftarrow s
q leftarrow t
t leftarrow

NAF derives not~s, not~r and p.

Completion semantics

The semantics of NAF remained an open issue until Keith Clark [1978] showed that it is correct with respect to the completion of the logic program, where, loosely speaking, "only" and leftarrow are interpreted as "if and only if", written as "iff" or "equiv".

For example, the completion of the four clauses above is

p equiv q and not~r
q equiv s or t
t equiv true
r equiv false
s equiv false

The NAF inference rule simulates reasoning explicitly with the completion, where both sides of the equivalence are negated and negation on the right-hand side is distributed down to atomic formulae. For example, to show not~p, NAF simulates reasoning with the equivalences

not~p equiv not~q or r
not~q equiv not~s and not~t
not~t equiv false
not~r equiv true
not~s equiv true

In the non-propositional case, the completion needs to be augmented with equality axioms, to formalise the assumption that individuals with distinct names are distinct. NAF simulates this by failure of unification. For example, given only the two clauses

p(a) leftarrow
p(b) leftarrow

NAF derives not~p(c).

The completion of the program is

p(X) equiv X=a or X=b

augmented with unique names axioms and domain closure axioms.

The completion semantics is closely related both to circumscription and to the closed world assumption.

Autoepistemic semantics

The completion semantics justifies interpreting the result not~p of a NAF inference as the classical negation neg p of p. However, Michael Gelfond [1987] showed that it is also possible to interpret not~p literally as "p can not be shown", "p is not known" or "p is not believed", as in autoepistemic logic. The autoepistemic interpretation was developed further by Gelfond and Lifschitz [1988] and is the basis of answer set programming.

The autoepistemics semantics of a pure Prolog program P with NAF literals is obtained by "expanding" P with a set of ground (variable-free) NAF literals Δ that is stable in the sense that

Δ = {not~p | p is not implied by P ∪ Δ}

In other words, a set of assumptions Δ about what can not be shown is stable if and only if Δ is the set of all sentences that truly can not be shown from the program P expanded by Δ. Here, because of the simple syntax of pure Prolog programs, "implied by" can be understood very simply as derivability using modus ponens and universal instantiation alone.

A program can have zero, one or more stable expansions. For example

p leftarrow not~p
has no stable expansions.

p leftarrow not~q
has exactly one stable expansion Δ = {not~q}

p leftarrow not~q
q leftarrow not~p
has exactly two stable expansions Δ1 = {not~p} and Δ2 = {not~q}.

The autoepistemic interpretation of NAF can be combined with classical negation, as in extended logic programming and answer set programming. Combining the two negations, it is possible to express, for example

neg p leftarrow not~p (the closed world assumption) and
p leftarrow not~neg p (p holds by default).


External links

  • Report from the W3C Workshop on Rule Languages for Interoperability. Includes notes on NAF and SNAF (scoped negation as failure).

Search another word or see negation by failureon Dictionary | Thesaurus |Spanish
Copyright © 2015, LLC. All rights reserved.
  • Please Login or Sign Up to use the Recent Searches feature