This report is the outcome of a Workshop on the Future Directions of Automated Deduction held in Chicago on April 20-21, 1996, and sponsored by the National Science Foundation (NSF). The workshop is one of several sponsored by the Division of Computer and Computation Research of NSF to provide for themselves and the relevant researchers an assessment of the opportunities in a given research area. For the researchers of the automated deduction (AD) field, the chance to consider together the future directions of AD research and development was of particular interest. The researchers see significant recent successes in several application areas and believe strongly that the successes are only beginning to arrive and that the economic and practical impact will be large. However, they see that research funding in the AD area has declined in the United States and are afraid of serious consequences should the decline continue. They also see the increased spending in Europe on AD research with resultant activity that has already eclipsed the United States effort. As a result of this effort, the Europeans researchers have already realized some application payoff and are convinced more is coming. The U.S. AD community sees a message in the above that needs communicating. With this mutual interest, a proposal was submitted to NSF, with the encouragement of Dr. S. Kamal Abdali, Program Director of Numeric, Symbolic and Geometric Computation, whose program is the primary funding source for AD research within NSF.
By budget and focus, the invitation list to the workshop was limited to a subset of the researchers in North America. To offset this limitation, a call for commentaries on the subject of the future directions of AD was issued to the AD community worldwide. The submissions (loosely edited for relevance) were posted on a Web page for workshop participants and others to read before the workshop meeting. The Web page is still in place at
Because the workshop was structured for discussion, few formal talks were scheduled. Dr. Abdali presented opening remarks that set the charge and perspective of the workshop. In his remarks he noted that funding from his program to AD from 1990 to the present (1996) has increased at roughly the rate of other areas in his program. Prof. Wolfgang Bibel (TH Darmstadt), invited to present the European perspective, spoke on ``European Efforts in Automated Deduction and Its Applications''. All other sessions were of discussion format, beginning with a session featuring the collected contributions and including parallel sessions in which future directions were considered by application area. The workshop spanned one and one-half days.
This report is a direct outcome of the workshop. In the limited time the workshop met, not all subjects were pursued, or when pursued not all were finalized. Thus, in addition to the findings of the workshop, lines under discussion are further developed in the report. The report also seeks to provide some needed background for the nonexpert. A draft of the report was critiqued by the workshop participants and revised based on the feedback. Participants sometimes differed on emphasis of material and the recommendations to be offered. Clearly, the report cannot reflect accurately and fully every participant's view of the field. Thus, the only person fully responsible for the assertions and views presented here is the author. All errors are the sole responsibility of the author.
Besides the contributions of the participants during the workshop weekend itself, there were many added contributions of time and effort without which the workshop and report would not have happened. First, the Steering Committee (Peter Andrews, Robert Boyer, Deepak Kapur Mark Stickel, and Larry Wos) was invaluable in all phases of this endeavor. Ed Clarke, Deepak Kapur, Ross Overbeek, Richard Waldinger, and Matt Kaufmann contributed summaries of the subarea meetings, and Matt Kaufmann contributed invaluable extended notes on the full meeting. The author is also grateful for many clear responses to technical questions by various members of the AD community, in particular Matt Kaufmann and Deepak Kapur. Many people provided useful critiques to the report draft, in particular Peter Andrews, Robert Constable, and Larry Wos. Larry Wos also provided the author with a valuable working paper on this subject. Gail Pieper's editorial comments were particularly appreciated. Those who took time to provide input in response to the worldwide call deserve special thanks. The perspective gained by the contributions was valuable to the workshop participants and the author of this report.
The entire automated deduction community is indebted to Dr. Abdali for providing the funding and the encouragement to convene a workshop that permitted this perspective on the automated deduction field.
It is important to emphasize that this study was commissioned and executed within the United States. Although we solicited information and opinions from the European community, the interchange was limited by time and funding. We make no claims that conditions presented here are universal or that the future directions and recommendations that we offer are the most appropriate assessments outside the United States.
Donald Loveland
Duke University
July 8, 1997