Negation as failure (NAF, for short) is a non-monotonic inference rule in logic programming, used to derive n o t p {\displaystyle \mathrm {not} ~p} (i.e. that p {\displaystyle p} is assumed not to hold) from failure to derive p {\displaystyle p} . Note that n o t p {\displaystyle \mathrm {not} ~p} can be different from the statement ¬ p {\displaystyle \neg p} of the logical negation of p {\displaystyle p} , depending on the completeness of the inference algorithm and thus also on the formal logic system. 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, in contrast with the strong (i.e. explicit, provable) negation.
Planner semantics 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. 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.
Prolog semantics In pure Prolog, NAF literals of the form n o t p {\displaystyle \mathrm {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 ← q ∧ n o t r {\displaystyle p\leftarrow q\land \mathrm {not} ~r}
q ← s {\displaystyle q\leftarrow s}
q ← t {\displaystyle q\leftarrow t}
t ← {\displaystyle t\leftarrow }
NAF derives n o t s {\displaystyle \mathrm {not} ~s} , n o t r {\displaystyle \mathrm {not} ~r} and p {\displaystyle p} as well as t {\displaystyle t} and q {\displaystyle q} .
Completion semantics 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 ← {\displaystyle \leftarrow } are interpreted as "if and only if", written as "iff" or " ≡ {\displaystyle \equiv } ". For example, the completion of the four clauses above is
p ≡ q ∧ n o t r {\displaystyle p\equiv q\land \mathrm {not} ~r}
q ≡ s ∨ t {\displaystyle q\equiv s\lor t}
t ≡ t r u e {\displaystyle t\equiv \mathrm {true} }
r ≡ f a l s e {\displaystyle r\equiv \mathrm {false} }
s ≡ f a l s e {\displaystyle s\equiv \mathrm {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 n o t p {\displaystyle \mathrm {not} ~p} , NAF simulates reasoning with the equivalences
n o t p ≡ n o t q ∨ r {\displaystyle \mathrm {not} ~p\equiv \mathrm {not} ~q\lor r}
n o t q ≡ n o t s ∧ n o t t {\displaystyle \mathrm {not} ~q\equiv \mathrm {not} ~s\land \mathrm {not} ~t}
n o t t ≡ f a l s e {\displaystyle \mathrm {not} ~t\equiv \mathrm {false} }
n o t r ≡ t r u e {\displaystyle \mathrm {not} ~r\equiv \mathrm {true} }
n o t s ≡ t r u e {\displaystyle \mathrm {not} ~s\equiv \mathrm {true} }
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 ) ← {\displaystyle p(a)\leftarrow }
p ( b ) ← t {\displaystyle p(b)\leftarrow t}
… excerpt ends here. Continue reading the full article.
