Inference

Forward and Backward Chaining

An inference problem can be formulated as follows:
  1. There is a set of sentences given as true, the hypotheses
  2. There is a sentence which it is desired to prove, call this the conclusion
  3. There are rules of inferecne that permit the deduction of additional sentences from given ones.
  4. Use the given rulkes of inference to deduce the conclusion from the hypotheses
For concreteness call the set of given sentences the Knowledge base KB, the conclusion g. Then we want to show KB |- g where |- stands for the use of our given inference procedure. This might for example be the generalised modus ponens of page 269 of AIMA.

In trying to construct a proof we can describe two apporaches. These are not exhaustive but they embody the two major "local " strategies.

Forward chaining
Given the knowledge base KB we can find an inference rule
Hypotheses
-----------
Conclusion
whose hypotheses unify with sentences in KB, we can then add the conclusion to the knowledge base (after making the substitutions required to math the hypotheses to the sentences of KB). This gives us a new KB in which more in known and we can repeat the process until g appears as the conclusion of one of these steps. We are then done.
Backward chaining
This time we start with g and look for an inference rule
Hypotheses
-----------
Conclusion
such that the conclusion can be unified with g. It then is enough to proof the hypotheses of this rule.

Note that Forward chaining can produce many irrelevant conclusions before arriving at a proof. Whereas backward chaining may pursue a misleading line of proof without some control.

Resolution

Resolution is a simple proof rule that is a complete inference procedure, at least in the sense that if the sentnces in the hypothesis lead to a contradiction resolution will determine that fact.

For literals pi and qi where pj and ~qk unify with unifier s

p1 \/ p2\/ ...\/pj\/ ...\/ pm
q1\/...qk\/... qn
-----------------------------------------------
subst(s, (p1\/p2 .. pj-1\/pj+1\/..\/pm\/q1\/..qk-1\/qk+1..\/qn))
Note that resolution can be used in either direction.

Canonical form for resolution

Sentences in FOL can be placed in Conjunctive normal form, meaning that they have the form
P \/ Q \/ R
Negations can appear P but no quantifiers.

The process by which this is done uses these steps.

  1. Eliminate implications
  2. Move not inwards
  3. Rename bound variables so that they are all distinct
  4. Move all quantifiers to the left
  5. Skolemize to remove quantifiers
  6. Distribute /\ over \/
  7. Flatten nested conjuncts and disjuncts

It should not have escaped your notice that Prolog uses resolution. .

Return to UG AI home page

Last Changed: 2 November 1995