#### 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*

**Example 5.29:**Consider the clauses from Example 5.28. Suppose the query is

*. Initially*

**ask**p*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.