papers for the volume. It was our feeling that the presentation in
the special session collectively portrayed the state-of-the-art, with
a sense of progress and high activity that exists in the field today.
We also feel that the papers presented in this volume are even
more successful at presenting the position and the momentum of
the field of ATP in 1983.
The first paper in the volume serves as the introduction and
overview to this volume as well as to the field of ATP. The papers
of Bledsoe, Boyer and Moore, and Wos and Winker have a tutorial
aspect and might be read next by those with little prior acquain-
tance with the field. A non-technical personal perspective of the
endeavor to automate theorem proving is offered by Hao Wang.
The papers by Lenat and Suppes outline substantial projects of
considerable interest to our community but whose published
reports have generally appeared in other settings. The remaining
papers are more technical but report substantial contributions to
the field.
We wish to thank the American Mathematics Society for their
interest in this developing field of Automated Theorem Proving,
both for the staging of the special session at the AMS Annual Meet-
ing in Denver, January 1983, and for their interest in publishing
this volume within the Contemporary Mathematics series. We
thank Tony Palermino for competent stewardship at AMS in bring-
ing this volume to press. Also, we thank David Mutchler at Duke
University for his time and expertise in guiding several of these
papers· through a balking text-processor and output device, we
thank Barbara Smith at the University of Texas, Austin, for typing
several papers under time pressure, and indirectly we thank those
who typed and supervised camera-ready copy preparation for indi-
vidual papers.
W.W. Bledsoe
D. W. Loveland
February 15, 1984
Previous Page Next Page