Page 143 - Intelligent Communication Systems

I 22 INTELLIGENT COMMUNICATION SYSTEMS
where x 4 is dependent on x\, x 2 and jc 3 and the relationship among variables Jtj, x 2,
;t 3, and x 4 is as follows:

Then expression (3) is represented as follows:

Thus, the existential quantifier 3 is eUminated./^, x 2, jc 3) is called a Skolem func-
tion. Expression (4) is called a Skolem standard form. In this way the clausal form
x 2, * 3,/(*i, x 2, x 3)
without existential quantifiers is obtained. In expression (4), P(x lf
is called a clause set.
10.4.5 Resolution Principle

In a clause set C, an operation that derives C tj from C, and C, by excluding P and
~P is called a resolution, where C, has an atomic formula P and C, has atomic for-
mula ~P. Adding C, y to C, a new clausal set C U {C,-,-} is created. This operation
is performed repeatedly until a null clause is derived. If a null clause is derived,
the clause set is unsatisfactory. This operation is called a resolution principle.
When a resolution principle is applied to C } = ~P v (2(1) and C 2 = ~(2 v J?(2), then
a new clause C 12 = ~PvR (3) is obtained.
A resolution principle has the same effect as a syllogism. According to the syl-
logism, a new logical expression P —» /? is derived from the expression P—*Q and
the expression Q-^R:

Through the resolution principle, Eq. (7) is obtained from Eqs. (5) and (6). There-
fore a syllogism is the same as the resolution principle.
Example 1: A clause set C l = {~P(a) v Q(b), ~Q(x)yR(y), P(z), ~R(t)}is given.
The resolution principle is applied as in Figure 10.13, where u is a unification and
u{b/x} means that b is assigned to x.

10.4.6 Logical Consequence
(Definition) Consider the logical expression (P 1? P 2,..., P n) and the logical expres-
sion Q. If (P], P 2,..., P n) is assumed to be true and Q becomes true, then Q
is a logical consequence of (P,, P 2,..., P n). If and only if a logical expression
(P,, P 2,,..,P n)-*Q is valid, then (P lt P 2,..., P n) -» Q is true. Then Q is a logical
consequence of (P,, P 2,..., P n). (Proof) Eq. (P,, P 2,..., P n) -» Q is assumed to
be valid. Then if (P,, P 2,..-, P n) is true, g is true. According to this definition,
Q is a logical consequence of (P l5 P 2,..., P n), On the other hand, if Q is a logi-
cal consequence of (P ls P 2,..., P n), Q is true when (P !r P 2,..., PJ is true. Therefore