6
D.W. LOVELAND
school exam problems within its domain (rectilinear diagrams).
Incidentally, running time was often comparable to high school
student time, e.g., about 20 minutes for a harder problem.
Simultaneously with the GTM effort the first efforts in the logic
. framework were occurring. Paul Gilmore and Hao Wang indepen-
dently sought to mechanically prove theorems in the predicate
calculus using not the heuristic methods of Newell and Simon but
methods derived from classical logic proof procedures. Both were
aware that known complete proof procedures need not be as
clumsy as implied by Newell and Simon. Gilmore was motivated by
Beth's semantic tableau technique. The procedure chosen was
crude by any standard (and acknowledged so by Gilmore) but it
was probably the first wo'rking mechanized proof procedure for
the predicate calculus and did prove some theorems of modest
difficulty (see Gilmore [Gil,Gi2]). Besides the novel undertaking
itself Gilmore was motivated by a desire to learn what computer
programming was like. He satisfied all his motivations and
effectively retired from the field (except for an enlightening
analysis of the GTM in [Gi3]).
Hao Wang explicitly sought to counter the impression Newell
and Simon imparted about the efficiency of proof procedures.
Wang initiated the program at IBM in the summer 1958 and contin-
ued his work at Bell Labs in 1959-1960 (see Wang [Wa1], [Wa2],
[Wa3]). Three programs were developed, one for propositional cal-
culus, one for a decidable part of the predicate calculus, and in
1959-1960 a third for all of predicate calculus. The
fi~t
program
proved 220 theorems of
Principia Mathematica
in 37 minutes {3
minutes actual computing time); an effective display that using
human-oriented techniques was not the only game in town. The
program was organized around Gertzen-Herbrand methods rather
than the semantic tableau approach of Gilmore. Of considerable
Previous Page Next Page