foundations of computational agents
The complete knowledge assumption, as discussed in Section 5.7, is the assumption that any statement that does not follow from a knowledge base is false. It also allows for proof by negation as failure.
The complete knowledge assumption for logic programs with variables and functions symbols requires axioms for equality, and the domain closure, and a more sophisticated notion of the completion.
Suppose a $student$ relation is defined by
$student(huan).$ |
$student(manpreet).$ |
$student(karan).$ |
The complete knowledge assumption would say that these three are the only students:
$student(X)\leftrightarrow X=huan\vee X=manpreet\vee X=karan.$ |
That is, if $X$ is $huan$, $manpreet$, or $karan$, then $X$ is a student, and if $X$ is a student, $X$ must be one of these three. In particular, $kim$ is not a student.
Concluding $\neg student(kim)$ requires proving $kim\ne huan\wedge kim\ne manpreet\wedge kim\ne karan$. To derive the inequalities, the unique names assumption is required.
The complete knowledge assumption includes the unique names assumption.
The Clark normal form of the clause
$p({t}_{1},\mathrm{\dots},{t}_{k})\leftarrow B.$ |
is the clause
$p({V}_{1},\mathrm{\dots},{V}_{k})\leftarrow \exists {W}_{1}\mathrm{\dots}\exists {W}_{m}{V}_{1}={t}_{1}\wedge \mathrm{\dots}\wedge {V}_{k}={t}_{k}\wedge B.$ |
where ${V}_{1},\mathrm{\dots},{V}_{k}$ are $k$ variables that did not appear in the original clause, and ${W}_{1},\mathrm{\dots},{W}_{m}$ are the original variables in the clause. “$\exists $” means “there exists”. When the clause is an atomic clause, $B$ is $true$.
Suppose all of the clauses for $p$ are put into Clark normal form, with the same set of introduced variables, giving
$p({V}_{1},\mathrm{\dots},{V}_{k})\leftarrow {B}_{1}.$ |
$\mathrm{\vdots}$ |
$p({V}_{1},\mathrm{\dots},{V}_{k})\leftarrow {B}_{n}.$ |
which is equivalent to
$p({V}_{1},\mathrm{\dots},{V}_{k})\leftarrow {B}_{1}\vee \mathrm{\dots}\vee {B}_{n}.$ |
This implication is logically equivalent to the set of original clauses.
Clark’s completion of predicate $p$ is the equivalence
$\forall {V}_{1}\mathrm{\dots}\forall {V}_{k}p({V}_{1},\mathrm{\dots},{V}_{k})\leftrightarrow {B}_{1}\vee \mathrm{\dots}\vee {B}_{n}$ |
where negation as failure ($\sim $) in bodies is replaced by standard logical negation ($\neg $). The completion means that $p({V}_{1},\mathrm{\dots},{V}_{k})$ is true if and only if at least one body ${B}_{i}$ is true.
Clark’s completion of a knowledge base consists of the completion of every predicate symbol.
For the clauses
$student(huan).$ |
$student(manpreet).$ |
$student(karan).$ |
the Clark normal form is
$student(V)\leftarrow V=huan.$ |
$student(V)\leftarrow V=manpreet.$ |
$student(V)\leftarrow V=karan.$ |
which is equivalent to
$student(V)\leftarrow V=huan\vee V=manpreet\vee V=karan.$ |
The completion of the $student$ predicate is
$\forall Vstudent(V)\leftrightarrow V=huan\vee V=manpreet\vee V=karan.$ |
Consider the following recursive definition:
$passed\mathrm{\_}each([],St,MinPass).$ |
$passed\mathrm{\_}each([C\mid R],St,MinPass)\leftarrow $ |
$passed(St,C,MinPass)\wedge $ |
$passed\mathrm{\_}each(R,St,MinPass).$ |
In Clark normal form, with variable renaming, this can be written as
$passed\mathrm{\_}each(L,S,M)\leftarrow L=[].$ |
$passed\mathrm{\_}each(L,S,M)\leftarrow $ |
$\exists C\exists RL=[C\mid R]\wedge $ |
$passed(S,C,M)\wedge $ |
$passed\mathrm{\_}each(R,S,M).$ |
Clark’s completion of $passed\mathrm{\_}each$ is
$\forall L\forall S\forall Mpassed\mathrm{\_}each(L,S,M)\leftrightarrow L=[]\vee $ |
$\exists C\exists R(L=[C\mid R]\wedge $ |
$passed(S,C,M)\wedge $ |
$passed\mathrm{\_}each(R,S,M)).$ |
Under the complete knowledge assumption, relations that cannot be defined using only definite clauses can now be defined.
Suppose you are given a database of $course(C)$ that is true if $C$ is a course, and $enrolled(S,C)$, which means that student $S$ is enrolled in course $C$. Without the complete knowledge assumption, you cannot define $empty\mathrm{\_}course(C)$, which is true if there are no students enrolled in course $C$. This is because there is always a model of the knowledge base where every course has someone enrolled.
Using negation as failure, $empty\mathrm{\_}course(C)$ can be defined by
$empty\mathrm{\_}course(C)\leftarrow course(C)\wedge \sim has\mathrm{\_}enrollment(C).$ |
$has\mathrm{\_}enrollment(C)\leftarrow enrolled(S,C).$ |
The completion of this is
$\forall Cempty\mathrm{\_}course(C)\leftrightarrow course(C)\wedge \neg has\mathrm{\_}enrollment(C).$ |
$\forall Chas\mathrm{\_}enrollment(C)\leftrightarrow \exists Senrolled(S,C).$ |
As a word of caution, you should be very careful when you include free variables within negation as failure. They usually do not mean what you think they might. The predicate $has\mathrm{\_}enrollment$ was introduced in the previous example to avoid having a free variable within a negation as failure. See Exercise 15.15.
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
$p(X)\leftarrow \sim q(X)\wedge r(X).$ |
$q(a).$ |
$q(b).$ |
$r(d).$ |
According to the semantics, there is only one answer to the query $\text{ask}\text{}p(X)$, which is $X=d$. As $r(d)$ follows, so does $\sim q(d)$ and so $p(d)$ logically follows from the knowledge base.
When the top-down proof procedure encounters $\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 \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 15.8.2), a sound proof procedure should delay the negated subgoal until the free variable is bound.
A more complicated top-down procedure is required when there are calls to negation as failure with free variables:
Negation-as-failure goals that contain free variables must not be selected in the negation-as-failure procedure of Figure 5.12 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
$p(X)\leftarrow \sim q(X)$ |
$q(X)\leftarrow \sim r(X)$ |
$r(a)$ |
and the query
$\text{ask}\text{}p(X).$ |
The completion of the knowledge base is
$p(X)\leftrightarrow \neg q(X)$ |
$q(X)\leftrightarrow \neg r(X)$ |
$r(X)\leftrightarrow 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.