2

D.W. LOVELAND

the ATP "Milestone" prize {Hao Wang) and the "Current Research"

prize (Lawrence Wos and Steven Winker). We do not dwell upon

their contributions, for they have review papers in this volume,

but seek to place their contributions, and those of others with

work presented here, in overall perspective. This is a history sum-

mary, not a tutorial; the technical aspect is not developed. Unfor-

tunately, space limitations prevent an encompassing document of

history, so we apologize in advance for all the significant develop-

ments and (many) important contributors not mentioned in this

review.

By automated theorem proving we mean the use of a computer

to prove non-numerical results, i.e. determine their truth (vali-

dity). Often (but not always, e.g. decision procedures) we may also

require human readable proofs rather than a simple statement:

"proved". Two modes of operation are used: fully automatic proof

searches and man-machine interaction ("interactive") proof

searches. The label ATP will cover both.

The first question of interest to mathematicians is: how good

are provers at this time? New mathematical results have been

discovered by automated provers. In 1967 SAM's lemma was

derived automatically during an interactive session with a

mathematician concerned with modular lattices (see [GOt]). The

mathematician recognized the lemma as the key to an open ques-

tion. Other open questions have been answered within finitely

axiomatizable theories. For example, in about 1980 Wos

et al.

answered positively the following open question, brought to their

attention by Kaplansky (see [WW2]). Does there exist a finite semi-

group which simultaneously admits of a nontrivial antiautomor-

phism without admitting a nontrivial involution? In set theory and

analysis progress is slower (not surprisingly) but definitely non-

trivial theorems such as Cantor's theorem (Andrews, this volume)