 Negation as failure

Negation as failure interprets failure of a specified proof search as a negative result. In the Prolog operation \+ Goal, the negative goal succeeds when trying Goal fails in finite time; it fails when Goal succeeds. A search that never finishes does not establish the negative result.^[ref]

For example, suppose a finite knowledge base records penguin(opus) and has no rule capable of deriving penguin(robin). A search for penguin(robin) finitely fails, so its negation succeeds under this operational rule. That result relies on the chosen knowledge base and search semantics. Adding the missing fact changes the result; an unrecorded fact in the outside world has not been independently disproved.

Stable model semantics gives a related model-based interpretation for negative rule premises through the stable model reduct. The rules $p\leftarrow \mathrm{not}q$ and $q\leftarrow \mathrm{not}p$ have two stable models, $\{p\}$ and $\{q\}$: in either candidate, the surviving rule forces exactly its one member. Neither atom follows by skeptical entailment. Operational finite failure and a chosen model semantics must therefore be distinguished when interpreting a negative rule.

Negation as failure is a concept primarily used in logic programming and non-monotonic reasoning, notably in the field of artificial intelligence and computational logic. It is a way of handling negation in a way that is consistent with the principle of closed world assumption (CWA). In classical logic, a statement can either be true or false, and the truth of a statement can be proven with evidence. However, in many practical applications, we often deal with incomplete knowledge about a system or domain.