Negation as failure (NAF, for short) is a non-monotonic inference rule in logic programming, used to derive
not~p
p
p
not~p
\negp
p
Negation as failure 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.
More generally, this kind of negation is known as weak negation,[1] [2] in contrast with the strong (i.e. explicit, provable) negation.
In Planner, negation as failure could be implemented as follows:
''if'' (''not'' (''goal'' p)), ''then'' (''assert'' ¬p)which says that if an exhaustive search to prove p fails, then assert ¬p.[3] This states that proposition p shall be assumed as "not true" in any subsequent processing. However, Planner not being based on a logical model, a logical interpretation of the preceding remains obscure.
In pure Prolog, NAF literals of the form
not~p
p\leftarrowq\landnot~r
q\leftarrows
q\leftarrowt
t\leftarrow
NAF derives
not~s
not~r
p
t
q
The semantics of NAF remained an open issue until 1978, when Keith Clark showed that it is correct with respect to the completion of the logic program, where, loosely speaking, "only" and
\leftarrow
\equiv
For example, the completion of the four clauses above is
p\equivq\landnot~r
q\equivs\lort
t\equivtrue
r\equivfalse
s\equivfalse
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
not~p\equivnot~q\lorr
not~q\equivnot~s\landnot~t
not~t\equivfalse
not~r\equivtrue
not~s\equivtrue
In the non-propositional case, the completion needs to be augmented with equality axioms, to formalize 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)\leftarrowt
NAF derives
not~p(c)
The completion of the program is
p(X)\equivX=a\lorX=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.
The completion semantics justifies interpreting the result
not~p
\negp
p
not~p
p
p
p
The autoepistemic 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
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\leftarrownot~p
p\leftarrownot~q
p\leftarrownot~q
q\leftarrownot~p
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
\negp\leftarrownot~p
p\leftarrownot~\negp
p