Automated deduction is concerned with the mechanization of the deductive process in the fullest meaning of that concept. This includes not only proving new mathematical results by computer, but formally verifying the correctness of (certain properties of) computer chip designs and programs, and even deducing the programs themselves from formal specifications of the task. Less obvious applications are use of automated inference tools within programming languages and within programs that produce scheduling algorithms and that optimize other programs. Some of the early work in this field is already part of the fabric of the artificial intelligence world. The machinery developed in this field is useful in inferring missing rules or facts in a problem specification (abduction) and generalizing from examples to full specifications (inductive inference, learning from examples), although we do not deal with these forms of reasoning in this report.
Some of our goals, such as fully mechanizing the proof capability of a mathematician, are still distant, but others, such as verifying computer chip designs, are already doable in part. This combination of profound, if distant, goals and important reachable goals make automated deduction an exciting field. The purpose of this report is to focus on the opportunities that seem both important and promising and to note especially those that have promise for near-term payoff.
We begin the report with a summary of the major accomplishments of the automated deduction field because not all readers of this report will be well versed in the history of the field. This is followed by the section on the future directions of automated deduction, first with a brief consideration of near-term opportunities and then with a discussion of the longer-term issues and opportunities. The latter presentation is organized by application area, where for convenience the core area of mathematics is considered an application area. To allow this section to focus on the technical issues, we use a separate section to treat the human resource issues, primarily the education and support of researchers and users of the technology. The conclusion is brief because the usual summary task is subsumed by the executive summary.
We have relegated all our acknowledgments to the preface. Here we simply note that this report exists because of the assistance of many people, to whom we again extend thanks.