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)
Previous Page Next Page