12.8 Complete Knowledge Assumption

To extend the complete knowledge assumption of Section 5.5 to logic programs with variables and functions symbols, we require axioms for equality, and the domain closure, and a more sophisticated notion of the completion. Again, this defines a form of negation as failure.

Example 12.45: Suppose a student relation is defined by

The complete knowledge assumption would say that these three are the only students; that is,

student(X)↔X=mary∨ X=john∨ X=ying.

That is, if X is mary, john, or ying, 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 ¬student(kim) requires proving prove kim≠mary ∧kim ≠john ∧kim≠ying. To derive the inequalities, the unique names assumption is required.

The complete knowledge assumption includes the unique names assumption. As a result, we assume the axioms for equality and inequality for the rest of this section.

The Clark normal form of the clause


is the clause

p(V1,...,Vk)←exist W1...exist Wm V1=t1∧...∧Vk =tk∧B.

where V1,...,Vk are k variables that did not appear in the original clause, and W1,...,Wm are the original variables in the clause. "exist " 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


which is equivalent to

p(V1,...,Vk)←B1∨ ...∨ Bn.

This implication is logically equivalent to the set of original clauses.

Clark's completion of predicate p is the equivalence

∀V1 ...∀Vk   p(V1,...,Vk) ↔B1∨ ...∨ Bn

where negations as failure () in the bodies are replaced by standard logical negation (¬). The completion means that p(V1,...,Vk) is true if and only if at least one body Bi is true.

Clark's completion of a knowledge base consists of the completion of every predicate symbol along with the axioms for equality and inequality.

Example 12.46: For the clauses

the Clark normal form is


which is equivalent to

student(V)←V=mary∨ V=john∨ V=ying.

The completion of the student predicate is

∀V   student(V)↔V=mary∨ V=john∨ V=ying.
Example 12.47: Consider the following recursive definition:

In Clark normal form, this can be written as

passed_each(L,S,M) ←L=[].
     exist C exist R L=[C|R]∧

Here we have removed the equalities that specify renaming of variables and have renamed the variables as appropriate. Thus, Clark's completion of passed_each is

∀L  ∀S  ∀M   passed_each(L,S,M) ↔L=[] ∨
     exist C exist R (L=[C|R]∧

Under the complete knowledge assumption, relations that cannot be defined using only definite clauses can now be defined.

Example 12.48: 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_course(C) that is true if there are no students enrolled in course C. This is because there is always a model of the knowledge base where someone is enrolled in every course.

Using negation as failure, empty_course(C) can be defined by


The completion of this is

∀C   empty_course(C)↔course(C)∧¬has_Enrollment(C).
∀C  has_Enrollment(C)↔exist S  enrolled(S,C).

Here we offer 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. We introduced the predicate has_Enrollment in the previous example to avoid having a free variable within a negation as failure. Consider what would have happened if you had not done this:

Example 12.49: One may be tempted to define empty_course in the following manner:

which has the completion

∀C empty_course(C)↔exist S  course(C)∧¬enrolled(S,C).

This is not correct. Given the clauses


the clause


is an instance of the preceding clause for which the body is true, and the head is false, because cs422 is not an empty course. This is a contradiction to the truth of the preceding clause.

Note that the completion of the definition in Example 12.48 is equivalent to

∀C empty_course(C)↔course(C)∧¬exist S  enrolled(S,C).

The existence is in the scope of the negation, so this is equivalent to

∀C empty_course(C)↔course(C)∧∀S  ¬enrolled(S,C).