13.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 13.52.

Consider the clauses

	$\displaystyle{p(X)\leftarrow\mbox{}\mbox{$\sim$}q(X)\wedge\mbox{}r(X).}$
	$\displaystyle{q(a).}$
	$\displaystyle{q(b).}$
	$\displaystyle{r(d).}$

According to the semantics, there is only one answer to the query $\mbox{{ask}~{}}~{}p(X)$ , which is $X=d$ . As $r(d)$ follows, so does $\mbox{$\sim$}q(d)$ and so $p(d)$ logically follows from the knowledge base.

When the top-down proof procedure encounters $\mbox{$\sim$}q(X)$ , it should not try to prove $q(X)$ , which succeeds (with substitution $\{X/a\}$ ). This would make the goal $p(X)$ fail, when it should succeed with $X=d$ . Thus, the proof procedure would be incomplete. Note that, if the knowledge base contained $s(X)\leftarrow\mbox{}\mbox{$\sim$}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 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.

Example 13.53.

Consider the clauses:

	$\displaystyle{p(X)\leftarrow\mbox{}\mbox{$\sim$}q(X)}$
	$\displaystyle{q(X)\leftarrow\mbox{}\mbox{$\sim$}r(X)}$
	$\displaystyle{r(a)}$

and the query

\displaystyle{{\mbox{{ask}~{}}~{}p(X).}}

The completion of the knowledge base is

	$\displaystyle{p(X)\leftrightarrow\neg q(X),}$
	$\displaystyle{q(X)\leftrightarrow\neg r(X),}$
	$\displaystyle{r(X)\iff X=a.}$

Substituting $X=a$ for $r$ gives $q(X)\leftrightarrow\neg X=a$ , and so $p(X)\leftrightarrow 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.

Artificial Intelligence 2E

13.8.1 Complete Knowledge Assumption Proof Procedures

Example 13.52.

Example 13.53.

Artificial
Intelligence 2E