Knowledge Representation in Clausal Form

1. Introduction

Logic studies the relationship of implication between assumptions and conclusions. It does not tell whether the assumptions are correct, likely, meaningful, etc., but can determine what follows from making those assumptions (what else would be true if the assumptions also were).

For instance, it would tell us that the assumptions:

Veronica likes logic. Veronica likes anyone who likes logic.

imply the conclusion

Veronica likes herself.

but not the conclusion

Veronica only likes people who like logic.

It would also tell us that the assumptions

All humans are immortal. Socrates is human.

imply the conclusion

Socrates is immortal.

regardless of the actual truth of the assumptions with respect to our real world

To demonstrate that assumptions imply a conclusion, it is helpful to construct a proof consisting of inference steps. For the proof to be convincing, the steps need to be direct and obvious, so the sentences should be unambiguous and their grammar should be as simple as possible.

The clausal form of logic fits this simplicity requirement. Its simplest sentences are atomic sentences, which name relationships between individuals:

likes(sweetie, rover) it_is_raining. gives(eve, adam, apple).

More complex sentences express that atomic conditions imply atomic conclusions:

likes(sweetie, rover) if likes(rover, sweetie). likes(veronica, X) if likes(X, logic).

We shall write ":-" instead of "if" in all that follows. X above is a variable that names any individual. Sentences can have several joint conditions or several alternative conclusions:

likes(sweetie, rover) or likes(sweetie, fido) :-: likes(sweetie, X).

(Sweetie likes Rover or Fido if Sweetie likes anything at all).

likes(veronica, X) :- student_of(veronica) and: likes(X, logic).

Sentences are also called clauses. In general, a clause expresses that a number (possibly zero) of joint conditions imply a number (possibly zero) of alternative conclusions. Conditions and conclusions express relationships among individuals. Because conditions are joint whereas conclusions are alternatice, we shall omit the words and and or in all that follows, and replace them by a comma, whose meaning is unambiguous since it is determined by what side of the "if" (:-) it appears in. Individuals may be fixed and named by words such as

sweetie, rover, logic, veronica, three

called constant symbols, or they may be arbitrary and named by variables such as

U, V, W, X, Y, Z, Three, Logic

(Notice that the particular symbol used is irrelevant to whether it is a constant or a variable: variables are denoted by an initial capital, thus Three denotes an arbitrary individual which can take any of a number of values (including 1, 2, 4), whereas three denotes a unique individual.

More complex names can be constructed through function symbols, e.g.: mother(rover) can be used to denote the individual who is the mother of the individual names rover. Notice the uniqueness presupposition implied both in the use of a function and in the use of the definite article "the": we are assuming rover has only one mother. We shall also agree that individuals in our world descriptions through logic will only admit one denomination. Thus, we cannot refer to the same individual as mother(rover) in one place and as sweetie in another, even though in the real world the mother of rover may be called sweetie. This is to avoid getting into the computationally expensive axioms of equality. If we admitted synonyms, we would then have to declare the different denominations as synonyms, and try them all in each proof concerning one of the denominations.

Examples of clauses with function symbols are:

likes(mother(X), X) sum(X, Y, +(X, Y)).

A consequence of our uniqueness-of-name convention is that, unlike in most other computer languages, functions do not evaluate. If we accepted that the value of mother(rover) is sweetie, or that the calue of +(3, 2) is 5, we would have two different names for the same individual. If we want to be able to calculate values, we should define them in sentences and use a separate argument for them:

mother_of(rover, sweetie). mother_of(able, eve).

plus(3, 2, 5). etc.

Notice that the uniqueness of rover's mother is no longer implicit in the syntax. Since we are now using relations to express functions (which are, of course, a special case of relations), it is up to us to not add another clause

mother_of(rover, duchesse).

which would result in rover having two mothers.

While functional expressions, in our convention, do not evaluate, they can still provide useful quick inference. From

likes(mother(X), X).

we can infer through the inexpensive operation of unification that rover's mother likes it, i.e.:

likes(mother(rover),rover).

An equivalent relational formulation of the same concepts is:

likes(X, Y) :- mother_of(X, Y).

With this latter formulation, arriving at the same conclusion takes one more inference step.

2. A Sample World Description in Clausal Form

mother( , ). father( , ). student( ). professor( ). female(X) :- mother(X, Y). male(X) :- father(X, Y). parent(X, Y) :- mother(X, Y). parent(X, Y) :- father(X, Y). grandparent(X, Y) :- parent(X, Z), parent(Z, Y). female(X), male(X) :- human(X).

3. A Formal Account of the Clausal Form of Logic

3.1 Syntax

A clause is an expression: b,...,b :- a,...,a

where b

,...,b

, a

,...,a

are atomic formulae, n

0 and m

0. The atomic formulae a

,...,a

are the joint conditions of the clause and b

,...,b

are the alternative conclusions. If the clause contains the variables X

,...X

then interpret it as stating that

for all X

,...,X

or...or b

if a

and...and a

If n=0 then interpret it as stating unconditionally that

for all X

,...,X

or...or b

":-" is usally ommitted in this case.

If m=0 then interpret it as stating that

for all X

,...X

it is not the case that
a

and...and a

(by convention, in this case we write ?- instead of :-)

If m=n=0 then write it as box and interpret it as a sentence which is always false.

an atom (or atomic formula, or prediction) is an expression of the form

p(t

,...,t

)

where p is an m-place predicate symbol, t

,...,t

are terms and m

0. Interpret the atom as asserting that the relation called p holds among the individuals called t

,...,t

. If m = 0, interpret it as asserting that p holds.

A term is a variable, a constant symbol or an expression of the form

f(t,...,t)

where f is an m-place function symbol, t

,...,t

are terms and m

The sets of predicate symbols, function symbols, constant symbols and variables are mutually disjoint sets. The various places of a predicate symbol or function symbol are also called its arguments.

Composite terms are needed in order to refer to infinitely many individuals using only finitely many clauses. For instance, the non-negative integers can be represented by the terms

0, s(0), s(s(0)),...

Where parentheses may become cumbersome, we can in Prolog declare that a functional symbol will be used as an operator in infix, prefix, or postfix notation. Thus, if "s" has been declared to be an operator in prefix notation, we can write the above terms as

0, s0, ss0,...

More commonly, we will use the postfix operator, ', so that the above terms can be written

0, 0', 0'',...

3.2 Semantics

While syntax deals with the grammar, or form, of sentences, and also with inference rules and proofs, semantics deals with meaning.

In symbolic logic, unlike in natural language, any meaning that might be associated with a predicate symbol, constant symbol, function symbol, or sentence is a relative to the collection of sentences which express all the relevant assumptions. Given a set of clauses which express all the assumptions concerning a problem domain, to understand any individual symbol or clause it is necessary to determine what is logically implied by the assumptions. The meaning of a predicate symbol, such as student, might be identified with the collection of all sentences which contain the predicate symbol and are logically impled by the assumptions.

It follows that all talk about meaning can be reexpressed in terms of logical implication. To define the semantics of the clausal form of logic, therefore, it suffices to define teh notion of logical implication.

In the clausal form of logic, to determine that a set of assumptions imply a conclusion we deny that the conclusion holds and show that the denial of the conclusion is inconsistent with the assumptions. The semantics of clausal form, therfore, reduces to the notion of inconsistency.

The inconsistency of a set of clauses can be demonstrated "semantically" by showing that no interpretation of the set of clauses makes tham all true, or it can be demonstrated "syntactically" by constructing a proof consisting of inference steps. The latter will be our approach.

3.2.1 The Universe of Discourse and Interpretations

If individuals are named by unique variable-free terms, then the universe of discourse, or Herbrand universe, of a set of clauses, which intuitively represents the collection of all individuals described by the clauses, can be identified with the colleciton of all variable-free terms which can be constructed from the constant symbols and function symbols occurring in the set of clauses. A candidate interpretation for a set of clauses can then be regarded as any assignment to each n-place predicate symbol occurring in the set of clauses of an n-place relation over the universe of discourse.

The interpretations that need to be considered in the semantic method of showing inconsistency of a set of clauses, by demonstrating that no interpretation makes all of its clauses true, can always be restricted to those whose domain of individuals consists of the universe of discourse. If the set of clauses contains no constant symbols, then it is necessary to include in the universe of discourse a single, arbitrary constant symbol, which formalises the assumption that at least one individual exists. In this case the universe of discourse consists of all variable-free terms which can be constructed from the given constant symbol and any function symbols which might occur in the set of clauses.

To specify an interpretation, it suffices to specify its effect on the truth or falsity of variable-free atomic formulae. An interpretation of a set of clauses, therefore, can be regarded as any assignment of either one of the two truth values

true and false

to every variable-free atom which can be constructed fromt he universe of discourse and the predicate symbols occurring in the set of clauses.

Definitions

A set of clauses S is inconsistent if-and-only-if (iff) it is not consistent. It is consistent iff all its clauses are true in some interpretation of S.

A clause is true in an interpretation of a set of clauses iff every variable-free instance of the clause, obtained by replacing variables by terms fromt he universe of discourse of S, is true in the interpretation. Otherwise the clause is false in the interpretation.

A variable-free clause is true in an interpretation I iff whenever all of its conditions are true in I, at least one of its conclusions is true in I. Equivalently, the clause is true in I iff at least one of its conditions is false in I or at least one of its conclusions is true in I. Otherwise, the clause is false in I.

Observations

Since the empty clause has neither conditions nor conclusions it cannot possible be true in any interpretation. It is only a clause which is self-inconsistent. To demonstrate the inconsistency of a set of clauses, it suffices to proce that it logically implies the obviously inconsistent empty clause. The empty set of clauses, however, is consistent. All clauses which belong to it are true in all interpretations, since it contains no clauses which can be false.

Definitions:

An instance of a clause is obtained by applying a substitution to the clause. A substitution is an assignment of terms to variables. Only one term is assigned to any given variable. It is convenient to represent a substitution as a collection of independent substitution components:

= t

, X

= t

,...,X

= t

}

The result of applying a substitution theta

to an expression E is a new expression E theta

which is just like E except that, wherever theta

contains a substitution component X

= t

and E contains an occurrence of the variable X

, the new expression contains an occurrence of t

. Different variables may be replaced by the same term.

4. Horn Clauses

Clauses containing at most one conclusion are called Horn clauses or definite clauses. It can be shown that any problem which can be expressed in logic can be expressed by means of Horn clauses.

Most programming formalisms resemble Horn rather than non-Horn clauses, and most of the problem solving models developed in AI can be regarded as models for problems expressed by means of Horn clauses. However, non-Horn clauses are indispensible in practice.

Exercises

Using the same vocabulary (i.e. predicate symbols, constants, and function symbols) as in our example above, express the following sentences in clausal form:
1. X is a mother of Y if X is female and X is a parent of Y.
2. X is a father of y if X is a male parent of Y.
3. X is human if Y is a parent of X and Y is human.
4. An individual is human if his or her mother is human and his or her father is human.
5. If a person is human then his (or her) mother is human or his (or her) father is human.
6. No one is his or her own parent.

Given clauses which define the relationships

father(X, Y)   (X is father of Y)
mother(X, Y)   (X is mother of Y)
male(X)        (X is male)
female(X)      (X is female)
parent(X, Y)   (X is parent of Y)
diff(X, Y)     (X is different than Y)

define the following additional relationships:

m(X)           (X is a mother)
f(X)           (X is a father)
s(X, Y)        (X is a son of Y)
d(X, Y)        (X is a daughter of Y)
gf(X, Y)       (X is a grandfather of Y)
sib(X, Y)      (X is a sibling of Y)

Let the intended interpretation of
```
hc(X)    be     X is a heavenly creature
wd(X)           X is worth discussing
star(X)         X is a star
comet(X)        X is a comet
planet(X)       X is a planet
near(X, Y)      X is near Y
ht(X)           X has a tail
```
1. Express in clausal form the assumptions:
  
  Every heavenly creature worht discussing is a star, planet or comet.
  Venus is a heavenly creature.
  Comets near the sun have tails.
  Venus is near the sun but does not have a tail.
2. What "obvious" missing assumption needs to be added to the clauses above for them to imply the conclusion
  
  Venus is a planet?
Using only the predicate symbols, numb, odd and even, the function symbol s, and the constant 0, express in clausal form
1. the conditions under which a number is even,
2. the conditions under which a number is odd,
3. that no number is both odd and even,
4. that a number is odd if its successor is even,
5. that a number is even if its successor is off,
6. that the successor of a number is odd if the number is even and that the successor is even if the number is odd.
Let the intended interpretation of

parity(X, odd) be X is odd
parity(X, even) be X is even.
Let the notion of opposite parities be expressed by the two clauses

opp(odd, even).
opp(even, odd).
Define the notion of a number being odd or even using only three additional clauses, two of them variable-free assertions.
Assume that arcs in a directed graph are described by assertions of the form

distance(r, s, t)
(the lenght of the arch from r to s is t).
Thus the assertion

distance(a, b, 3).
describes the arc from a to b. Assume also that the relationship

Z is X+Y
which holds when X+Y=Z, is already given. Using only one clause, extend the definition of the relationship dist(X, Y, Z) so that it expresses that there is a path of length Z from X to Y.
There are four different variable-free atoms which can be constructed from the vocabulary of the following clauses:

L1: likes(veronica, logic).
L2: likes(veronica, X) :- likes(X, logic).
L3: ?-likes(X, Y), likes(Y, Y).
Consequently there are 16 different interpretations of this set of clauses. How many of these interpretations make both L1 and L2 true? How many make L3 true? How many make all of L1-L3 true?

This looks like a trivial observation now, but it will become a point to remember when you start programming. Because logic is so close to language, it is easy to attach "meaning" to mnemonic symbols, which are no more than symbols for a computer, and to attach truth value to assumptions. It is best to view assumptions as holding in an imaginary, hypothetical world, so as not to endow them with prejudices about our own. How closely we are able to describe a subset of our own world in logic becomes then a matter of skill rather than of wishful thinking.

$RCSfile: $ $Revision: $ $Date: $