The genesis of the collection of papers presented in this
volume is a special session on automated theorem proving (ATP),
held in conjunction with the annual meeting of the American
Mathematical Society in Denver, January, 1983, to honor several
research leaders in the field of ATP. Hao Wang received the first
Milestone Prize for his pioneering work in the early years of
research in ATP and Lawrence Wos and Steven Winker received the
Current Research Prize for recent and ongoing work. The cita-
tions appear in this volume with papers by the recipients. It is
anticipated that both awards will be given periodically at a yet
undetermined interval.
A secondary purpose for the special session was to bring to the
attention of the mathematics research community the status of
work in ATP.
is clear from the work of several research groups
that the state has been reached where serious thought can be
given by mathematicians to the possibilities of computer-aided
proof discovery. (Fully automated proof, and theorem, discovery
remains a goal but current success, in some ways quite impressive,
is still very limited.) It is our hope that some active mathemati-
cians will choose to accept the challenge this field extends and
work, probably with an existing research group in ATP, to extend
our capabilities towards frontier mathematics.
The papers in this volume derive primarily from the presenta-
tions by invited speakers at the special sessions, although invita-
tions were extended to Wu Wen-Tsun and Patrick Suppes to submit
Previous Page Next Page