Third edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2023 is now available (including the full text).
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.
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.
q(X) ←∼r(X)
r(a)
and the query
The completion of the knowledge base is
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.
