Preface 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. It 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 vii
Previous Page Next Page