#### 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 bi in a body fails if ∼bi has been derived. A negation ∼bi in a body fails if bi has been derived.

1: 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←b1∧...∧bm"
12:                                         bi∈C for all 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←b1∧...∧bm" ∈KB
18:                                         either for some bi,∼bi∈C
19:                                         or some bi=∼g and g ∈C
20:                               C←C∪{∼h}
21:           until no more selections are possible
Figure 5.11: Bottom-up negation as failure proof procedure

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.