Near-Term Opportunities

In any discussion of future opportunities and accomplishments, the inevitable question is when such accomplishments will appear. Estimating arrival times for innovations is, in general, a risky business to be avoided. Our concession to this interest will be limited to comments on possible near-term directions and achievements (roughly five to seven years ahead). In this time frame we look to existing successes for the seed of new successes. These include further use of Otter (and maybe E-SETHEO, a competing first-order system new to the scene, whose reason for note we consider later) for general first-order reasoning applications. Otter may have the widest distribution and broadest range of applications of automated deduction (AD) systems yet developed. However, many other systems now have user communities of their own, some sizable: Nqthm, ACL2, and RRL, for example, and the higher-order logic systems HOL, Nuprl, Isabelle, PVS, Coq, and TPS. Some have already had sufficient impact on real-world problems that industry is adopting and aiding the development of the systems. For example, ICL of England is developing a commercial version of HOL. That so many provers have significant user communities is an indication that the level of accomplishment in automated deduction has jumped noticeably in the past five years and that applications are expected to continue and show increasing sophistication.

There is some interest in making AD systems available to a wider community in the near future, and even some consideration of commercial automated reasoning systems. To succeed, the system must have a targeted clientele to which the system can be tailored. Tailoring involves selection of a theorem prover (most often a fully automated version will be appropriate) and design of a good user interface. The user interface includes choice of input and output languages, and manner of providing search information with the problem input. User interface issues are discussed near the beginning of Section 3.2.5. The best current example of a proof system ready for a wider audience is the geometry program(s) of Chou et al. It has a well-specified problem domain, the deduction power, user-friendliness, and multiple hardware versions. However, to be effective in the education realm, its primary application area, a software educational support package may be needed. Some type of application support package may be a requirement of all application systems using theorem provers; certainly that seems true of today's AD systems.

The verification community is now exhibiting real-world success. We noted earlier that microcontrollers are being verified in commercial applications, as are various concurrent systems and transaction systems. Safety critical systems are being formally verified. The growing practicality of this technology is recognized by NASA in the convening of a workshop on formal methods where practicing engineers can meet with leading researchers (more on this below). There is no denying that AD technology has increased in visibility and usefulness in the past few years. This pace will continue and applications will come faster as the examples of success cause more application engineers to investigate the current opportunities. However, this does not mean that the field now breaks open its cornucopia. The major problem of handling induction, for example, is as tough as ever and will yield only to slow, determined work on many fronts. It has taken a long time by industrial standards (not relative to the development of the other mechanism for reasoning, by evolution) to get to the state we now enjoy, and progress from here may be as slow as fundamental work has traditionally been. But now each accomplishment may have a noticeable incremental impact on applications because it can be added on top of systems already productive. For the above reasons we treat the specifics of future verification research in the subsection on longer-term opportunities, while acknowledging here that any accomplishment that ``shows up early'' likely will be immediately welcomed in the applications world.

We must remark that in the United States the danger exists that, because of funding problems, some of the systems named above will not continue to be developed. This may be true even of verification systems that have the most immediate and focused economic reasons for development and have shown some strong recent success. At present, it seems likely that Europe will keep its funding level high. This situation may hurt the United States commercially in a decade or so, but for the intellectual outcome it is nice that funding continues somewhere.

In the area of program synthesis we consider two outstanding systems that will have near-term impact, both mentioned in the preceding section. The impact is quite different in the two cases. For AMPHION the interest is in an exportable system design, whereas for the KIDS program the continued development of the existing system, as well as the applications that will follow, of most interest. Both systems are examples of highly constrained search, the secret to harnessing AD in program synthesis with current technology. We somewhat arbitrarily focus on AMPHION here and postpone discussion of KIDS until the section on the longer-term view.

AMPHION derives programs from graphical specifications (input through a menu-driven regimen), which is translated into a theorem whose proof defines a program that makes extensive use of existing software from an in-system library. The theorem prover, an Otter-like prover written at SRI, works with an application domain theory that contains axioms encoding (in this application) basic properties of solar-system astronomy and axioms giving specifications of the available subroutines. The proof is constrained to be constructive so that a program can be developed from the proof. The methodology is derived from work of Manna and Waldinger [66]. The system is (in effect) an extremely sophisticated expert system, but uses inference capability well beyond that associated with the ``expert system'' label.

We recognize that the existence of a library of subroutines that interact to address a problem class is not common. With a few successes like AMPHION, task groups might be motivated to construct such subroutine libraries. This is, of course, a longer-term opportunity. A major concern now is how to identify other points of application for AMPHION-like projects. Specific industries do learn through meetings, trade papers, and the like, that particular problems can be addressed with the new technology. This is a major way in which expert systems technology spread. For the past four years, NASA has held an annual workshop to promote such technology transfer for applications of mechanized formal methods (specification and verification) to safety-critical systems. The existence of such workshops underscores the real-world value of some AD technologies. Perhaps a workshop in applied program synthesis could feature the AMPHION technology. Other methods of technology transfer are briefly discussed in the section on human resource use. Our point is that AMPHION incorporates a powerful technology that is likely to have other applications at the present level of our capabilities in AD. Exploring other possible applications will also cause the capabilities to be expanded, thereby providing a useful focus and helping to teach the subfield how to scale up to the more complex problems.

Addressing other possibilities, there may be near-term products that come from the wedding of computer algebra and AD techniques. Likewise, meaningful application of AD techniques to model checking methods of verification may already be under way. In the next section, we discuss both subjects (and others) but suppress any temptation to guess timing beyond the conservative calls we have already made.