How Computers Think - Robots Unlimited: Life in a Virtual Age - page 189

sub-problem, because the program knows that this new sub-problem can
form the second part of a chain with “ A is true implies that B is true ”,
resulting in the following proof:
A is true
But A is true implies that B is true
Therefore B is true
But B is true implies that C is true
Therefore C is true
So A is true implies that C is true
Backwards chaining works in a similar way. Given the problem of prov-
ing that “ A is true implies that C is true ”, the backward-chaining method
seeks a theorem of the form “ B is true implies that C is true ” and, if one
is found, the expression “ A is true implies B is true ”issetupasanew
sub-problem, because solving this new sub-problem, combined with the
knowledge that “ B is true implies that C is true ”, provides a solution to
the original problem.
Each of these three methods of improving the efficiency of perfor-
mance of the Logic Theory Machine is independent of the others. They
can be used in sequence, one working on the sub-problems generated by
another, resulting in the various sub-problems becoming intermediate
expressions in a proof sequence.
The proof process is rather like growing a tree. Each application of
each method can be thought of as a branch of the tree. At the end of
each branch is the updated list of axioms, theorems and sub-problems.
This whole process continues until a proof has been found, or there is
no more available computer time, or the computer runs out of mem-
ory, or there are no untried problems on the sub-problem list (in which
case the program will never find a proof ). In the days of Newell and
Simon's original work on the Logic Theory Machine, the prospect of
running out of time was a real one—a simple proof of four steps re-
quired about ten seconds, while one example of five steps needed about
12 minutes. Clearly deep and complex proofs would have taken for-
ever in 1956, but in fact the program was able to prove, within a rea-
sonable amount of time, 38 of the first 52 theorems found in Principia
Mathematica .