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