Third edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2023 is now available (including the full text).

5.5.2.2 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 ∼a is selected, a new proof for atom a is started. If the proof for a fails, ∼a succeeds. If the proof for a succeeds, the algorithm fails and must make other choices. The algorithm is shown in Figure 5.12.

non-deterministic procedure NAFTD(KB,Query)
2:           Inputs
3:                     KB: a set of clauses that can include negation as failure
4:                     Query: a set of literals to prove Output
5:                     yes if completion of KB entails Query and no otherwise
6:           Local
7:                     G is a set of literals
8:           G←Query
9:           repeat
10:                     select literal l∈G
11:                     if (l is of the form ∼a) then
12:                               if (NAFTD(KB,a) fails) then
13:                                         G ←G \ {l}
14:                               else
15:                                         fail
16:                     else
17:                               choose clause l ←B from KB
18:                               replace l with B in G
19:                     
20:           until G={}
21:           return yes
Figure 5.12: Top-down negation-as-failure interpreter
Example 5.29: Consider the clauses from Example 5.28. Suppose the query is ask p. Initially G={p}.

Using the first rule for p, G becomes { q, ∼r}.

Selecting q, and replacing it with the body of the third rule, G becomes {∼s, ∼r}.

It then selects ∼s and starts a proof for s. This proof for s fails, and thus G becomes { ∼r}.

It then selects ∼r and tries to prove r. In the proof for r, there is the subgoal ∼t, and thus it tries to prove t. This proof for t succeeds. Thus, the proof for ∼t fails and, because there are no more rules for r, the proof for r fails. Thus, the proof for ∼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←p. The algorithm does not halt for the query ask p. The completion, p↔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 ∼p, as it does not follow from the completion.