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