foundations of computational agents
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.
Consider the clauses
According to the semantics, there is only one answer to the query , which is . As follows, so does and so logically follows from the knowledge base.
When the top-down proof procedure encounters , it should not try to prove , which succeeds (with substitution ). This would make the goal fail, when it should succeed with . Thus, the proof procedure would be incomplete. Note that, if the knowledge base contained , the failure of would mean succeeding. Thus, with negation as failure, incompleteness leads to unsoundness.
As with the unique names assumption (Section 13.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.
Consider the clauses:
and the query
The completion of the knowledge base is
Substituting for gives , and so . Thus, there is one answer, namely , 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.