Part of the consideration of future directions for the automated deduction field is concern with investment in the training of both future researchers and users of the technology. We first consider the education of researchers. The primary means of developing researchers should remain the funding of students on individual research grants. Grants are subjected to review and competition in the award process, which serves as effective quality control. We see a need for grants to include postdoctoral positions. This will permit ``cross-pollination'' in the classic manner of other disciplines; people learn in depth one approach to a subject and then can be embedded in a laboratory with an alternative approach. This in-depth exposure to multiple techniques is important as AD systems become more sophisticated. For example, the techniques of planning and proof abstraction might be beneficial to proof by induction, and each is a difficult research problem on its own. We expect that the number of postdoctoral positions would be small, as the job market itself is small.
In addition to funds for emerging scientists we urge the use of sabbaticals for researchers to visit AD centers and centers of application technologies. Sabbaticals are common for university researchers, but supplemental funds often are needed to allow a year's stay rather than four months. Government contract laboratories and commercial enterprises do not traditionally allocate funds for professional leaves. We encourage such institutions both to accept, with funding when possible, researchers from other environments and to send their own researchers to other laboratories. We encourage funding agencies to facilitate such exchanges by providing grants explicitly for such purposes. It is important that the grants be valid for international use, as in many areas excellent (sometimes the best) work is now being done overseas.
A different aspect of human resource development and use is the question of allocation of research grants. A case can be made for increased support of leading AD research centers, particularly as provers become more complex and multifaceted. Many facets will undergo continued development, in effect creating a constantly evolving system, with the obvious advantages and problems. The theorem prover would become the center of a community of researchers, who would come both to use the system and to enhance it. These researchers would be drawn not only by the machine but by the opportunity to be embedded in a community of kindred spirits. As mentioned earlier, this situation is similar in many ways to the lifestyle of high-energy physicists and lessons in funding that research should be applied here. (There are many tricky issues here we cannot address; when funds are awarded for research away from the university, the university usually does not get overhead. However, universities need overhead funds from grants and at various levels of subtlety discourage grants that do not cover overhead. While universities are going to have to learn to accommodate such grants, the need to help the universities cannot be ignored.) On the other hand, some researchers disagree with the need to focus any special funds on centers. They argue that software is exportable and the systems can come to the researcher as well as the converse. In this they are correct; users in general will have their own AD system. It is on the technological edge, with evolving systems, that the community effect likely will intensify. Innovations now are usually augmentations, not new basic procedures. Integration of these improvements often requires intimate involvement with the system, an on-site activity.
When debating the value of increased support of AD research centers, we must also recall that excellent research is still being done by isolated researchers and that support must continue for the best of these efforts. As just one example of strong research in a more isolated setting, we mention the work of David Plaisted at the University of North Carolina (UNC). The sole AD researcher at UNC, David is developing some very different and interesting ideas on incorporating semantics into theorem provers [90]. Also, at least at present, systems can still be developed by one or two people. Analytica is one such example (although it used a substantial system from another domain) and METEOR [4], built by Owen Astrachan at Duke University, rivaled SETHEO for performance until very recently, when the engineering resources of the SETHEO team did prevail.
The user of AD technology has different goals and hence different needs in education. The user often is concerned only with existing technology and may have time limits on the development process for the application being explored. Application-oriented workshops provide a low-cost way for potential users to see existing uses of AD technology. Such workshops are useful for those whose interests match well the applications already in place. We have already mentioned some effective workshops in this regard. One such workshop (series) is the NASA workshop on formal methods for safety-critical systems. In Europe and Japan, conferences in applications of logic programming are leading to increased applications for Prolog in domains such as business and engineering design. We have suggested earlier that a workshop be organized around the program synthesis from software libraries as for AMPHION.
We note, however, that for those with an application idea but without in-house expertise for its development, workshops are inadequate. They would be well served by extended time at selected AD centers or application sites. Examples of AD centers with application experience are Argonne and SRI. Application sites often have proprietary interest in the product and may be inaccessible for working visits. However, NASA may be an example of a place where access is possible. Since use of AD tools and methods in products is rare, employers are likely to be reluctant to commit fully to exploration of ideas that do have potential. The existence of funds for collaboration between user and AD centers, by agencies concerned with technology transfer, will maximize the likelihood that a commercial idea sees the light of day.