# 5.6.2 Proof Procedures for Negation as Failure

## Bottom-Up Procedure

The bottom-up procedure for negation as failure is a modification of the bottom-up procedure for definite clauses. The difference is that it can add literals of the form $\mbox{\sim}p$ to the set $C$ of consequences that have been derived; $\mbox{\sim}p$ is added to $C$ when it can determine that $p$ must fail.

Failure can be defined recursively: $p$ fails when every body of a clause with $p$ as the head fails. A body fails if one of the literals in the body fails. An atom $b_{i}$ in a body fails if $\mbox{\sim}b_{i}$ can be derived. A negation $\mbox{\sim}b_{i}$ in a body fails if $b_{i}$ can be derived.

Figure 5.11 gives a bottom-up negation-as-failure interpreter for computing consequents of a ground KB. Note that this includes the case of a clause with an empty body (in which case $m=0$, and the atom at the head is added to $C$) and the case of an atom that does not appear in the head of any clause (in which case its negation is added to $C$).

###### Example 5.31.

Consider the following clauses:

 $\displaystyle{p\leftarrow\mbox{}q\wedge\mbox{}\mbox{\sim}r.}$ $\displaystyle{p\leftarrow\mbox{}s.}$ $\displaystyle{q\leftarrow\mbox{}\mbox{\sim}s.}$ $\displaystyle{r\leftarrow\mbox{}\mbox{\sim}t.}$ $\displaystyle{t.}$ $\displaystyle{s\leftarrow\mbox{}w.}$

The following is a possible sequence of literals added to $C$:

 $\displaystyle{t}$ $\displaystyle{\mbox{\sim}r}$ $\displaystyle{\mbox{\sim}w}$ $\displaystyle{\mbox{\sim}s}$ $\displaystyle{q}$ $\displaystyle{p}$

where $t$ is derived trivially because it is given as an atomic clause; $\mbox{\sim}r$ is derived because $t\in C$; $\mbox{\sim}w$ is derived as there are no clauses for $w$, and so the “for every clause” condition of line 18 of Figure 5.11 trivially holds. Literal $\mbox{\sim}s$ is derived as $\mbox{\sim}w\in C$; and $q$ and $p$ are derived as the bodies are all proved.

## Top-Down Negation-as-Failure Procedure

The top-down procedure for the complete knowledge assumption proceeds by negation as failure. It is similar to the top-down definite-clause proof procedure of Figure 5.4. This is a non-deterministic procedure (see the box) that can be implemented by searching over choices that succeed. When a negated atom $\mbox{\sim}a$ is selected, a new proof for atom $a$ is started. If the proof for $a$ fails, $\mbox{\sim}a$ succeeds. If the proof for $a$ succeeds, the algorithm fails and must make other choices. The algorithm is shown in Figure 5.12.

###### Example 5.32.

Consider the clauses from Example 5.31. Suppose the query is $\mbox{{ask}~{}}~{}p$.

Initially, $G=\{p\}$.

Using the first rule for $p$, $G$ becomes $\{q,\mbox{\sim}r\}$.

Selecting $q$, and replacing it with the body of the third rule, $G$ becomes $\{\mbox{\sim}s,\mbox{\sim}r\}$.

It then selects $\mbox{\sim}s$ and starts a proof for $s$. This proof for $s$ fails, and thus $G$ becomes $\{\mbox{\sim}r\}$.

It then selects $\mbox{\sim}r$ and tries to prove $r$. In the proof for $r$, there is the subgoal $\mbox{\sim}t$, and so it tries to prove $t$. This proof for $t$ succeeds. Thus, the proof for $\mbox{\sim}t$ fails and, because there are no more rules for $r$, the proof for $r$ fails. Therefore, the proof for $\mbox{\sim}r$ succeeds.

$G$ is empty and so it returns yes as the answer to the top-level query.

Note that this implements finite failure, because it makes no conclusion if the proof procedure does not halt. For example, suppose there is just the rule $p\leftarrow\mbox{}p$. The algorithm does not halt for the query $\mbox{{ask}~{}}~{}p$. The completion, $p\iff p$, gives no information. Even though there may be a way to conclude that there will never be a proof for $p$, a sound proof procedure should not conclude $\mbox{\sim}p$, as it does not follow from the completion.