Prof R. Williams
Artificial Intelligence


	  DRAWING INFERENCES USING PREDICATE CALCULUS


The key rules of inference used for both forward and backward chaining
are the following:

Modus Ponens			Given:  	p
------------					(if p q)

				Conclude: 	q

where p and q are any expressions which have a true/false value.
Any expression of the form (if p q) is called an implication, with p
called the antecedent and q the consequent of the implication.

Universal Specialization	Given:		(forall (x) (P x))
------------------------
				Conclude:	(P a)

where P is any predicate and a is any constant.  The idea is that we may
substitute a specific value for the variable x.


To see how we may use these to draw conclusions, consider the following
two sentences (which we consider to be part of some larger knowledge base):

1.  "Every person loves somebody."

2.  "John is a person."

We translate these into predicate calculus as follows:

1.  (forall (x) (if (person x)
	(exists (y) (and (person y) (loves x y)))))

2.  (person John)

We may apply universal specialization to sentence 1 to derive the conclusion
(which can be considered a new sentence)

3.  (if (person John) (exists (y) (and (person y) (loves John y))))

We may then apply modus ponens to sentences 2 and 3 to obtain

4.  (exists (y) (and (person y) (loves John y)))

which says

    "There is somebody whom John loves."


A key ingredient of the process of using the combination of modus ponens
and universal specialization to draw conclusions is determining what
to substitute for variables in order to make certain subexpressions
match.  In the above example, there may be many values we might imagine
substituting for x in sentence 1 (e.g., Mary), but only the substitution of
John for x allows us to arrive at sentence 4.  The idea is that once we
decide to try to use modus ponens using sentence 1 and sentence 2, we must
find a substitution which makes the antecedent of the implication
given by sentence 1 match the expression given by sentence 2.  This process
of specifying a substitution for variables which makes a set of expressions
identical to one another is called "unification."