Robotics Reference
In-Depth Information
Clearly this process, which Newell and Simon called the British Museum
Algorithm, will eventually lead to a proof of the target theorem or to
a solution of the given problem, provided one exists. This is because
eventually the program will construct all possible proofs in a systematic
manner but in a random order, checking each time to eliminate duplicate
attempts and to see if the target theorem has been proved. The difficulty
with this approach is that working in a randommanner is not guaranteed
to provide success. The process will generate far more useless sequences
of expressions than useful ones, and for any difficult or complex theorem
or problem the program is likely to run out of time or out of computer
memory for storing all of the newly generated expressions. Nevertheless,
the method is sufficiently powerful that one of the first 246 theorems
generated and proved by the Logic Theory Machine was the same as
one from Chapter 2 of Principia Mathematica ,anditwasprovedbythe
program in only four steps, while three more of the theorems from the
same source were proved in six steps, and one more was proved in eight
steps. Thus, five out of the first 246 theorems to be generated and proved
by the Logic Theory Machine, using this random approach, are amongst
those published by Russell and Whitehead.
In order to improve the efficiency of the process the Logic Theory
Machine needed a way to radically improve the order in which possi-
ble proofs of theorems and solutions to problems were generated. Three
methods were developed for searching for a proof or solution, called sub-
stitution, detachment 7 and chaining.
The substitution method finds an axiom or a previously-proved theo-
rem that can be transformed into the expression that needs to be proved.
The transformation can be accomplished, for example, by a series of sub-
stitutions that are similar to those employed in proofs in high school
algebra.
The detachment method replaces a problem expression by a new sub-
problem, that has been chosen so that if the new sub-problem is solved,
its solution provides a proof for the original problem expression.
The chaining method is based on two techniques called forward chain-
ing and backward chaining. If the problem expression is “ A is true im-
plies that C is true ”, forward chaining is used to search for an axiom or
theorem of the form “A is true implies that B is true”. If one is found
then the expression “B is true implies that C is true ”issetupasanew
7 See also footnote 5.
Search WWH ::




Custom Search