5.6 Complete Knowledge Assumption

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

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 ∼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 can be derived. A negation ∼bi in a body fails if bi can be derived.

1: procedure Prove_NAF_BU(KB)
2:      Inputs
3:          KB: a set of clauses that can include negation as failure      
4:      Output
5:          set of literals that follow from the completion of KB
6:      Local
7:          C is a set of literals      
8:      C:=⁢{}
9:      repeat
10:          either
11:          select r∈KB such that
12:          r is “h←⁢b1∧⁢…∧⁢bm”
13:          bi∈C for all i, and
14:          h∉C;
15:          C:=⁢C∪{h}
16:          or
17:          select h such that ∼h∉C and
18:          where for every clause “h←⁢b1∧⁢…∧⁢bm” ∈KB
19:          either for some bi,∼bi∈C
20:          or some bi=∼g and g∈C
21:          C:=⁢C∪{∼h}
22:      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.31.

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 18 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.

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.

1: non-deterministic procedure Prove_NAF_TD(KB,Query)
2:      Inputs
3:          KB: a set of clauses that can include negation as failure
4:          Query: a set of literals to prove      
5:      Output
6:          yes if completion of KB entails Query and f⁢a⁢i⁢l otherwise
7:      Local
8:          G is a set of literals      
9:      G:=Query
10:      repeat
11:          select literal l∈G
12:          if l is of the form ∼a then
13:               if Prove_NAF_TD⁢(KB,a) fails then
14:                   G:=⁢G∖{l}
15:               else
16:                   fail               
17:          else
18:               choose clause “l←⁢B” in KB with l as head
19:               G:=⁢G∖{l}∪B          
20:      until G={}
21:      return yes
Figure 5.12: Top-down negation as failure interpreter
Example 5.32.

Consider the clauses from Example 5.31. Suppose the query is 𝖺𝗌𝗄 ⁢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 so 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. Therefore, 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 𝖺𝗌𝗄 ⁢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.