Page 139 - Intelligent Communication Systems

I I 8 INTELLIGENT COMMUNICATION SYSTEMS

(3) Rename bound variables so they do not conflict with one another:

(4) Convert form (3) to a standard form:

(5) Convert a matrix to a conjunctive normal form:

A predicate logical expression is satisfactory when it has at least a value T. A
logical expression is valid when it always has a value T. A logical expression is
unsatisfactory when it always has a value F.

10.4.3 Herbrand Universe and the Herbrand Theorem
To prove that a clausal set is unsatisfactory, it is necessary to consider every inter-
pretation in a specific domain. However, this is difficult to achieve. Instead, a
Herbrand universe that is equivalent to the above interpretation is considered.
A Herbrand universe is defined as follows.
(1) HQ = {a set of individual constants in a clause set C}. Unless there are
no individual constants, it is assumed that H 0 = {a}.
(2) H i+l = H { U {a set off(s l, s 2, s n)}, where/is all of the functions used in
C and 8, is every ground instance in H t.
(3) H(C) = H X
Example 1: C = {P(a), Q(x)}, so H 0 = {a}.
Example 2: C= {P(a), Q(f(x)), R(x)}, so H 0 = {«}, H l = {a, /(a)}, and H 2 =
{«,/(«),/(/(<*))}.
An atomic formula of a clause set C, where an element of H(C) is assigned to
a variable of the atomic formula, is called a ground instance. A set composed of
all of the ground instances is called a Herbrand base. Because an atomic formula