Artificial Intelligence
Prof. R. Williams


	   INTRODUCTION TO FORWARD AND BACKWARD CHAINING
		  IN RULE-BASED DEDUCTION SYSTEMS


Consider the two statements:

	"Every human is fallible."
	"John is human."

We treat the first of these as a rule, which we write as the predicate
calculus sentence (in implicit quantifier form):

	(if (human ?x) (fallible ?x))

The second we consider a fact, which we write as the predicate calculus
sentence:

	(human john)

In order to see whether the rule applies to john, we need to see whether
the two logical expressions

	(human ?x)
	(human john)

can be made identical to each other by an appropriate substitution for
the variable ?x in both expressions.  This matching process is called
unification.  If we can unify a fact with the antecedent of a rule,
then we can conclude that the consequent is true once the same
substitution has been made in it.  In this case, the substitution
we seek is {?x/john}, and we can then apply the rule to conclude
the new fact

	(fallible john)

The process just described is called forward chaining because we used
the rule in the forward direction.  We can also use rules in a backward
direction, as follows:  Suppose we begin with the goal of establishing
the truth of the logical formula

	(fallible john)

given our one fact and our one rule.  In backward chaining mode, the
rule is interpreted to say:  "To show that (fallible ?x) is true,
show that (human ?x) is true."  Since the objective is to show
(fallible john), we thus want to find an appropriate substitution
for the variable ?x so that the two expressions

	(fallible john)
	(fallible ?x)

can be made identical to each other.  Obviously, substituting john for ?x
works, and we are left with the objective of showing that

	(human john)

is true.  Since this turns out to be a fact in our knowlege base, we have
thus succeeded in proving what we set out to prove, namely, (fallible john).


More generally, our rules may contain several antecedents and we may have
several facts and rules.  For example, suppose that we have the facts

	(imitates john mary)
	(eats mary pizza)

and the rule

	(if (and (imitates ?x ?y) (eats ?y ?z)) (eats ?x ?z))

In this case, the substitution {?x/john, ?y/mary, ?z/pizza}
unifies the pair of expressions

	(imitates john mary)
	(imitates ?x ?y)

as well as the pair of expressions

	(eats mary pizza)
	(eats ?y ?z)

Thus we may forward chain from the rule to conclude the new fact

	(eats john pizza)


For backward chaining we assume that we begin with the objective of
showing that (eats john pizza).  Since this unifies with (eats ?x ?z),
this tells us the rule can be applied if we can show that both

	(imitates john ?y)

and

	(eats ?y pizza)

are true for some appropriate choice of ?y.  Clearly, substituting
mary for ?y in these makes them identical to our two facts, so we
can thus conclude that (eats john pizza) is indeed true.