Backward Chaining

In backward chaining, if it is desired to prove the conclusion C of a clause, the system tries to do so by proving the premises P1 ... Pn.

&forall x CAR(x) &and RED(x) &rarr EXPENSIVE(x)

Given this axiom, an attempt to prove that BMW1 is expensive would be reduced to the subproblems of proving that it is a car and that it is red.


  1. Infinite loops. For example, consider transitivity:

    &forall x &forall y &forall z GREATER(x,y) &and GREATER(y,z) &rarr GREATER(x,z)

  2. The system has to keep reproving (and failing to prove) the same mundane facts.

Contents    Page-10    Prev    Next    Page+10    Index