#### 5.5.2.1 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 *∼p* to the set *C* of
consequences that have been derived; *∼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

*∼b*has been derived. A negation

_{i}*∼b*in a body fails if

_{i}*b*has been derived.

_{i}**Procedure**NAFBU(

*KB*)

2:

**Inputs**

3:

*KB*: a set of clauses that can include negation as failure

**Output**

4: set of literals that follow from the completion of

*KB*

5:

**Local**

6:

*C*is a set of literals

7:

*C←{}*

8:

**repeat**

9:

**either**

10:

**select**

*r∈KB*such that

11:

*r*is "

*h←b*"

_{1}∧...∧b_{m}12:

*b*for all

_{i}∈C*i*, and

13:

*h∉C;*

14:

*C←C∪{h}*

15:

**or**

16:

**select**

*h*such that

*∼h ∉C*and

17: where for every clause "

*h←b*"

_{1}∧...∧b_{m}*∈KB*

18: either for some

*b*

_{i},∼b_{i}∈C19: or some

*b*and

_{i}=∼g*g ∈C*

20:

*C←C∪{∼h}*

21:

**until**no more selections are possible

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.28:**Consider the following clauses:

*p←q∧∼r.*

*p←s.*

*q←∼s.*

*r←∼t.*

*t.*

*s←w.*

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

*t,*

*∼r,*

*∼w,*

*∼s,*

*q,*

*p,*

where *t* is derived trivially because it is given as an atomic clause; *∼r* is derived because *t∈C*; *∼w* is derived as there
are no clauses for *w*, and so the "for every clause" condition of
line 17
of Figure 5.11 trivially holds. Literal *∼s*
is derived as *∼w∈C*; and *q* and *p* are derived as the bodies are all
proved.