Full text of the second edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2017 is now available.

### 12.8.1 Complete Knowledge Assumption Proof Procedures

The top-down proof procedure for negation as failure with the variables and functions is much like the top-down procedure for propositional negation as failure. As with the unique names assumption, a problem arises when there are free variables in negated goals.

**Example 12.50:**Consider the clauses

*p(X)←∼q(X)∧r(X).*

*q(a).*

*q(b).*

*r(d).*

According to the semantics, there is only one answer to the query
* ask p(X)*, which is

*X=d*. As

*r(d)*follows, so does

*∼q(d)*and so

*p(d)*logically follows from the knowledge base.

When the top-down proof procedure encounters
*∼q(X)*, it should not try to prove *q(X)*, which succeeds (with substitution
*{X/a}*), and so fail *∼q(X)*. This would make the goal
*p(X)* fail, when it should succeed. Thus, the proof procedure would be incomplete. Note that,
if the knowledge base contained *s(X) ←∼q(X)*, the failure of *q(X)*
would mean *s(X)* succeeding. Thus, with negation as failure,
incompleteness leads to
unsoundness.

As with the unique names assumption [Section 12.7.2], a sound proof procedure should delay the negated subgoal until the free variable is bound.

We require a more complicated top-down procedure when there are calls to negation as failure with free variables:

- Negation as failure goals that contain free variables must be delayed until the variables become bound.
- If the variables never become bound, the goal
**flounders**. In this case, you cannot conclude anything about the goal. The following example shows that you should do something more sophisticated for the case of floundering goals.

**Example 12.51:**Consider the clauses:

*p(X) ←∼q(X)*

*q(X) ←∼r(X)*

*r(a)*

and the query

**ask**p(X).The completion of the knowledge base is

*p(X) ↔¬q(X),*

*q(X) ↔¬r(X),*

*r(X) ↔X=a.*

Substituting *X=a* for *r* gives *q(X) ↔¬X=a*, and so *p(X) ↔X=a*.
Thus, there is one answer, namely *X=a*, but
delaying the goal will not help find it. A proof procedure should analyze the cases
for which the goal failed to derive this answer. However, such a
procedure is beyond the scope of this book.