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

It was called variously the “Logic Theorist” and the “Logic Theory Ma-
chine”, and was able to deduce the proofs to theorems in a form of
logic called the propositional calculus, a system of logic propounded by
Bertrand Russell and Alfred Whitehead in their classic three-volume se-
ries Principia Mathematica which was published in 1910-1913. 5
The Logic Theory Machine was able to use the axioms and inference
rules proposed by Russell and Whitehead, together with and , not , or and
implies (which are called connectives), in order to operate on mathemat-
ical theorems that had already been proved, and thereby to generate new
theorems. Starting with an expression that it wants to prove, i.e., a new
theorem, and with the set of five axioms (which it had been told are true)
and with the theorems it had already proved (which it knew to be true),
the Logic Theory Machine would apply the three inference rules again
and again until it generated the desired mathematical expression, the one
that it wanted to prove.
If a computer were to be given an infinite amount of time and mem-
ory we could use the Logic Theory Machine to prove any provable the-
orem and to solve any solvable problem. 6 The process would simply be
this:
1. Check to see if any of the existing expressions (including the orig-
inal axioms and the already-proved theorems) is an exact match of
what we want to prove. If so, the task has been completed and the
program should stop and print out or display its proof.
2. If none of the existing axioms or already-proved theorems is an
exactmatchofwhatwewanttoprove,applyeachoftheinfer-
ence rules to all the existing expressions and to all pairs of existing
expressions (but with the restriction that the program should not
apply a rule twice to the same expression or to the same pair of ex-
pressions). This process will create new expressions that are known
to be true, and the program can then go back to Step 1.
5 The system was based on a set of five logical axioms—expressions that are always true, for
example: [ p is true or ( q is true or r is true )] implies that [ q is true or ( p is true or r is true )]. In
order to use these axioms to create new theorems from known ones, the system also employs three
rules of inference, for example the rule of detachment , which states that if A is true ,andif“ Aimplies
B ”is true ,then B is also true . Russell and Whitehead attempted to show that it is possible to derive
all mathematical truths from their five axioms and three inference rules.
6 Proving a theorem and solving a problem are very similar tasks from a logic perspective. In
solving a problem the solver hypothesizes a solution and then tests it—this testing process is akin to
proving a theorem. If the test is successful, the “theorem” (i.e., that the hypothesized solution works)
has been proved.