Contemporary Mathematics
Volume 29, 1984
AUTOMATED
TIIEOREM-PROVING:
A QUARTER-CENTURY REVIEW
Donald W. Loveland
1
This opportunity to review the events and concepts that shape
the present field of automated theorem proving (ATP) is particu-
larly attractive because of the timing; twenty-five years ago
(1957), the first publication appeared that reported results of a
computer program that proved theorems. The paper, "The Logic
Theory Machine" by Newell, Shaw and Simon [NS1], presented a
program that could prove some theorems in the sentential cal-
culus of
Principia Mathematica.
(A program to prove theorems in
additive arithmetic was written by Martin Davis in 1954 but led to
no publication.) The paper by Newell, Shaw and Simon, the
stimulus of a 1956 Dartmouth conference on "artificial intelli-
gence", and the increasing availability to researchers of then
high-powered computers (i.e., substantial memory and speed) led
to a spurt of activity that initiated the field. This activity has con-
tinued, slower than some anticipated yet faster than others
expected, with an occasional shift in approach. It is this activity
that we summarize.
A primary purpose of this paper is to provide an overview for
the mathematics community of the history of ATP so as to better
understand the contributions to this field by the first winners of
1 Computer Science Dept., Duke University, Durham. NC 27706.
1
© 1984 American Mathematical Society
0271-4132/84 $1.00
+
$.25 per page
http://dx.doi.org/10.1090/conm/029/749237
Previous Page Next Page