Prof R. Williams				Artificial Intelligence


	     LOGICAL INFERENCES THROUGH BACKWARD CHAINING


Backward chaining is a particular way to draw logical inferences from
a predicate calculus knowledge base using modus ponens and universal
specialization.  In forward chaining each time a new sentence
(predicate calculus formula) is added to the knowledge base, all
possible conclusions resulting from the use of modus ponens and
universal specialization are also added.  This is clearly impractical
for large databases.  In contrast, pure backward chaining never adds
sentences to the knowledge base; instead, it allows responses to
specific queries made against the database.  Thus backward chaining
may be better thought of as a sophisticated database retrieval mechanism.

As an example, suppose that our database has the following sentences in it:

F1:	(on block-1 table)
F2:	(on block-2 block-1)
F3:	(on block-3 block-1)
F4:	(on block-4 block-2)
F5:	(on block-5 table)
F6:	(above lamp table)
F7:	(color table beige)
F8:	(color block-1 red)
F9:	(color block-2 white)
F10:	(color block-3 blue)
F11:	(color block-4 green)
F12:	(color block-5 blue)
F13:	(color lamp yellow)
F14:	(next-to lamp block-1)
R1:	(if (on ?x ?y) (above ?x ?y))
R2:	(if (and (above ?x ?y) (above ?y ?z)) (above ?x ?z))
R3:	(if (next-to ?x ?y) (next-to ?y ?x))

(You may find it helpful to draw a picture of the scene described.)

Suppose we want to ask:  "Is there something on the table?"

We view this as setting as a goal to show that there exists something
that is on the table; i.e., we want to show (exists (x) (on x table)).
To do this formally, using implicit quantifier form to match our database,
the query to our backward chaining program becomes

	(retrieve '(on ?x table))

which is interpreted as setting up the following list of goals:

	Goals: (on ?x table)

Here our list has only one formula in it.  Later we will see examples
where there are several formulas in this list.

Why do we use ?x here instead of a skolem constant?  For reasons we'll
discuss later, skolemization of the goal formula is handled as if there
were an additional "not" around it.

The backward chaining process then proceeds as follows:

(1) First determine whether any sentence in the database unifies with the
    goal sentence; if it does, the goal sentence trivially follows from the
    sentences in the database.  Furthermore, the variable bindings used
    to unify the two can tell us more than just "Yes, the goal sentence
    follows from the sentences in the knowledge base," as we'll see below.

(2) If no sentence unifies with the goal sentence, find an implication
    whose consequent unifies with the goal sentence and now try to
    show that the antecedent (with variables appropriately bound)
    follows from the sentences in the knowledge base.  We'll see how
    this is handled more precisely in examples below.

For our example,

	Goals: (on ?x table)

we find that the very first fact in the database,

	(on block-1 table)

unifies with it.  (As an implementation detail, we assume that any
searches through the database proceed according to the order in which
the sentences are listed.)  The MGU is {?x/block-1}.  Thus we can conclude
that the answer is "Yes, there is something on the table."  Moreover,
we can do better than that; our full answer might be something like
"Yes, block-1 is on the table."  The variable substitution appearing
in the MGU actually specifies a particular thing that is on the table.
In general, backward chaining can be used to answer questions of the
form "Is there a ...?" not just with "yes" or "no", but with much more
specific information.

The above example only used step 1 of the backward chaining process.
Here's a query using step 2 as well:  "Is block-1 next to the lamp?"

	(retrieve '(next-to block-1 lamp))

which leads to the goal list

	Goals: (next-to block-1 lamp)

We find that the goal sentence does not unify with any sentences in the
database, but it does unify with the consequent of

	(if (next-to ?x ?y) (next-to ?y ?x))

I.e., the two sentences

	(next-to block-1 lamp)
	(next-to ?y ?x)

unify, with MGU = {?x/lamp, ?y/block-1}.

We thus replace our original goal formula with the formula resulting
from making these substitutions in the antecedent, so our goal list
becomes

	Goals: (next-to lamp block-1)

We now do the same process with this, discovering that this new goal
unifies with the fact

	(next-to lamp block-1)

in the database.  Thus the answer to the original question is "yes."

Another query: "Is there something next to the lamp."

	(retrieve '(next-to ?z lamp))

This gives us the goal list

	Goals: (next-to ?z lamp)

This is similar to the previous one.  Step 1 fails, but step 2 discovers
that the goal formula and the consequent of

	(if (next-to ?x ?y) (next-to ?y ?x))

unify, with MGU = {?x/lamp, ?y/?z}.  The new goal list is then

	Goals: (next-to lamp ?z)

Applying step 1 to this, we discover that this new goal formula unifies
with the fact

	(next-to lamp block-1)

in the database, with MGU = {?z/block-1}.  Thus the answer to the
question is "Yes, block-1 is next to the lamp."

Things get more involved if we have a goal formula which involves a
conjunction (i.e., "and").  Suppose we ask "Is there something blue
on the table?"  This becomes

	(retrieve '(and (color ?x blue) (on ?x table)))

Instead of trying to unify this entire formula with either facts or
implication consequents in the database, we treat this almost as
if it consisted of the separate queries

	(retrieve '(color ?x blue))
	(retrieve '(on ?x table))

However, we also must be sure that the same thing gets substituted for
?x in both formulas.  (It would not do to find one thing that is blue
and another that is on the table.)  The way this is done is to try to
satisfy the first goal formula, and then try to satisfy the second
using the variable bindings already established for the first.
Thus we begin with the goal list

	Goals: 	(color ?x blue)
		(on ?x table)

Whenever we have more than one formula in the goal list, we always
work on just the top one, either eliminating it via step 1 or
replacing it by one or more other formulas via step 2.
Thus we begin by considering just the top goal

	(color ?x blue)

Using step 1 alone, we first arrive at {?x/block-3}.
We then substitute accordingly into all remaining goal formulas.
This leaves us with the goal list

	Goals: (on block-3 table)

We discover that this does not unify with any fact in the database, nor
does it unify with any implication consequents in the database.  Thus
we must now back up and try a different way to satisfy the first goal

	(color ?x blue)

The next possibility for this is {?x/block-5}, so we then work on

	Goals:	(on block-5 table)

This works, so the answer is "Yes, block-5 is blue and on the table."

The backtracking being discussed here can be viewed as performing
depth-first exploration of a suitably defined graph.

Now consider the question "Is there something next to something yellow?"

	(retrieve '(and (next-to ?u ?v) (color ?v yellow)))

This gives us the goal list

	Goals:	(next-to ?u ?v)
		(color ?v yellow)

We begin with the top goal

	(next-to ?u ?v)

which unifies with the fact

	(next-to lamp block-1)

with MGU = {?u/lamp, ?v/block-1}.  Making this substitution in the
second goal we are left with the goal list

	Goals: (color block-1 yellow)

but this fails.  Thus we back up and look for the next way we could
satisfy the original top goal

	(next-to ?u ?v)

We use the implication

	(if (next-to ?x ?y) (next-to ?y ?x))

in the database to backward chain.  An MGU for

	(next-to ?u ?v)
	(next-to ?y ?x)

is {?u/?y, ?v/?x}.  In this case our new goal list is

	Goals:	(next-to ?v ?u)
		(color ?v yellow)

which unifies with

	(next-to lamp block-1)

with MGU = {?u/block-1, ?v/lamp}.  We then must make this substitution
in (color ?v yellow), and are left with

	Goals: (color lamp yellow)

This unifies with a fact in the database, and we are done.  The
answer is "Yes, block-1 is next to the lamp, which is yellow."

If we had asked "Is there something yellow with something next to it?"
we would have formulated this as

	(retrieve '(and (color ?v yellow) (next-to ?u ?v)))

giving us the goal list

	Goals:	(color ?v yellow)
		(next-to ?u ?v)

and the search would have been conducted slightly differently, beginning
with first finding something yellow and then checking whether something
is next to it.  The order in which the conjuncts are specified in the goal
formula thus can make a difference in terms of just how the search is
carried out.  In some cases, this can have a big effect on the efficiency
of the resulting search.

Now consider the question "Is there something next to something green?"

	(retrieve '(and (next-to ?u ?v) (color ?v green)))

or

	Goals:	(next-to ?u ?v)
		(color ?v green)

This starts out just as before.  The top goal

	(next-to ?u ?v)

unifies with the fact

	(next-to lamp block-1)

with MGU = {?u/lamp, ?v/block-1}, so we want

	(retrieve '(color block-1 green))

but this fails.  Thus we back up and look for the next way we could
satisfy the top goal

	(next-to ?u ?v))

which leads to

	Goals:	(next-to ?v ?u)
		(color ?v green)

The top goal unifies with

	(next-to lamp block-1)

with MGU = {?u/block-1, ?v/lamp}, and we then consider

	Goals:	(color lamp green)

This fails, so we back up to see if there is another way to try to satisfy

	(retrieve '(next-to ?v ?u))

Backward chaining using the appropriate implication in the database
leads us to consider

	Goals:	(next-to ?u ?v)
		(color ?v green)

However, we're already considering ways to do this on this search path.
Just as when converting a state-space search graph to a tree, we never
want a path that has a loop in it; thus we don't try to extend this
path.  We thus back up to see if there is any other way to satisfy the
original top goal

	(next-to ?u ?v)

Since there isn't, we declare failure.  The answer is "No, there isn't
anything next to something green."

Some other queries we may discuss in class:

	(retrieve '(and (color ?x yellow) (above ?x table)))

	(retrieve '(and (color ?x green) (above ?x table)))

	(retrieve '(and (above ?x table) (color ?x green)))

	(retrieve '(and (color ?x gray) (above ?x table)))

	(retrieve '(and (color ?x beige) (above ?x table)))

	(retrieve '(and (color ?x red) (color ?y yellow) (next-to ?x ?y)))

	(retrieve '(and (color ?x beige) (next-to ?x lamp)))