Negation as failure

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 eg 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 (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 eg 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.