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