foundations of computational agents
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 to the set of consequences that have been derived; is added to when it can determine that must fail.
Failure can be defined recursively: fails when every body of a clause with as the head fails. A body fails if one of the literals in the body fails. An atom in a body fails if can be derived. A negation in a body fails if can be derived.
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 , and the atom at the head is added to ) and the case of an atom that does not appear in the head of any clause (in which case its negation is added to ).
Consider the following clauses:
The following is a possible sequence of literals added to :
where is derived trivially because it is given as an atomic clause; is derived because ; is derived as there are no clauses for , and so the “for every clause” condition of line 18 of Figure 5.11 trivially holds. Literal is derived as ; and and are derived as the bodies are all proved.
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 is selected, a new proof for atom is started. If the proof for fails, succeeds. If the proof for succeeds, the algorithm fails and must make other choices. The algorithm is shown in Figure 5.12.
Consider the clauses from Example 5.31. Suppose the query is .
Using the first rule for , becomes .
Selecting , and replacing it with the body of the third rule, becomes .
It then selects and starts a proof for . This proof for fails, and thus becomes .
It then selects and tries to prove . In the proof for , there is the subgoal , and so it tries to prove . This proof for succeeds. Thus, the proof for fails and, because there are no more rules for , the proof for fails. Therefore, the proof for succeeds.
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 . The algorithm does not halt for the query . The completion, , gives no information. Even though there may be a way to conclude that there will never be a proof for , a sound proof procedure should not conclude , as it does not follow from the completion.