Logic Foundation of Artificial Intelligence - Advanced Artificial Intelligence - page 49

positive-ground-literal clause P 1 ∨ P 2 ∨ … ∨ P n that follows from KB, there is at
least one ground literal P i which is entailed by KB.

In other words, CWA(KB) is inconsistent if and only if there are positive
ground literals P 1 , P 2 , …, P n such that KB |= P 1 ∨ P 2 ∨…∨ P n and KB|≠P i for each
1≤ i ≤ n.
Example 2.2 Let KB = { P(A)∨P(B) }. It is obvious that CWA(KB) is
inconsistent.

Example 2.3 Let KB = {∀x(P(x )∨Q(x )), P(A), Q(B)}. With respect to the
atom A and B, KB will be augmented with ¬P(B) and ¬Q(A), and will resulted
in a consistent theory. However, if there is an atom C, then the resulted theory is
inconsistent since it is both (P(x )∨Q(x )) |≠ P(C) and (P(x )∨Q(x ))|≠Q(C).

Generally speaking, theory augmented by the CWA might be inconsistent.
However, if the knowledge base KB is composed of Horn clauses and is
consistent, then the augmented theory CWA(KB) is also consistent. I.e., we have
the following theorm:
Theorem 2.2 If the clause form of KB is Horn and consistent, then the CWA

augmentation CWA(KB) is consistent.

The condition that KB be Horn is too strong for many applications. In fact,
according to Theorem 2.1, such a condition is not absolutely necessary for the
CWA augmentation of KB to be consistent. An attempt of weakening this
condition leads to the idea of the CWA with respect to a predicate P. Under that
convention, if KB is Horn in some predicate P and P is not provable from KB,
then we can just add the negation of P into the set KBasm. Here, we say that a set
of clauses is Horn in a predict P if there is at most one positive occurrence of P in
each clause.
For example, suppose KB is {P(A)∨Q(A), P(A)∨R(A)}. It is obvious that KB
is Horn in the predicate P, even though both P(A)∨Q(A) and P(A)∨R(A) are not
Horn clauses. Set KBasm = {¬P(A)}, then we have KB∪KBasm|=Q(A) and
KB∪KBasm|=R(A), and thereby get a consistent augmented theory CWA (KB)
with respect to the predicate P.