Executive Summary

Automated deduction (AD) is one of the most advanced and technically deep of the many technologies that constitute computer science. It is concerned with software that performs deduction--from the fast simple deductions of a type checker and the efficient exploration of models to fully automated deduction and complex deductive interactions with users in a high-level language. The field lies at an interface with mathematics, logic, and computing theory as well as with practice. It has contributed fundamental ideas to these fields as well as drawing heavily from them.

Automatic deduction has spawned a number of useful tools and systems, and it holds great promise of making substantial progress on some of the most challenging problems in computer science and engineering--how to improve the reliability of systems, how to build secure software, how to increase productivity in software production. In the mathematics world some previously unsolved problems have been solved by or with the assistance of an AD system.

The attempt to automate deduction is about forty years old. Recent accomplishments have given the field new visibility and given the public evidence of meaningful progress. The most notable event is the discovery by a computer of a proof for the Robbins algebra conjecture in 1996. In areas related to mathematics it is rare to get public press, but this accomplishment reached the New York Times Science section front page. We note below some additional achievements that have had definite impact on their application area. Still other areas affected by the AD field are not discussed because of lack of space; nevertheless, they are tightly linked to AD and in many cases arose from AD advances. Examples are domain theory, type theory, programming logics, deductive databases, formal methods, logics of knowledge, knowledge representation and zero-knowledge proofs.

We use the term automated deduction for automated theorem provers, counterexample (model) generation, and consequence generators. This includes both fully automated and interactive systems. We note that AD systems may establish truth of a statement by means other than a formal proof (a listing of steps that are given or follow from previous steps), for example by a decision procedure such as computing and comparing terms in an equation. Likewise, disproofs are frequently counterexamples.

Achievements

We first consider some recent achievements within the AD field.

• The Robbins algebra conjecture was established as a theorem by the system EQP developed by William McCune of Argonne National Laboratory in 1996. The proof was obtained with the computer in fully automatic mode. The problem had been investigated by a number of top mathematicians and was a favorite open conjecture of the late mathematician Alfred Tarski, one of the foremost logicians of this century.
• The study of mathematical structures called quasigroups has been significantly advanced by the use of several different deduction programs. Both the existence and the nonexistence of various classes of quasigroups have been shown.
• Several open problems regarding axioms for equivalential calculi and other logics and algebras have been solved over the past decade or so.
• A geometry theorem prover exists that proves a large class of difficult theorems in Euclidean and non-Euclidean geometries. A version exists for the PC and Macintosh that is user-friendly enough to be suitable for the nonspecialist. Particularly noteworthy are the readable proofs produced.

Not all the achievements are in the mathematics arena. The verification/specification domain employs AD systems in almost pure form, usually in the interactive mode.

• The specifications of communications networks too complex for human analysis have been verified by computer. This work includes both the determination that the specifications are consistent (that a communications network can exist that meets all requirements) and proof that a resultant designed network meets key properties of the specifications.
• Safety-critical hardware and software have been checked by AD systems as to whether key requirements are met. These systems are too complex to allow unaided human verification.
• Some complete commercial microcontrollers, parts of commercial microprocessors, and their key algorithms have been verified mechanically, although the largest commercial chips are not verifiable using AD systems at present and probably in the near future.

In the following application areas the AD program is a smaller part of the systems package.

• A program synthesis system that depends heavily on formal methods and formal reasoning has derived computer programs for scheduling logistics tasks that outperform the scheduling programs in use. The increase in performance is sometimes striking.
• Another program synthesis system uses a theorem prover to assemble subroutines from an existing library and produce working code. The programs aid satellite guidance.
• Programming languages such as Prolog, CLP($\cal{R}$), and ECLiPSe are built around a deductive inference engine. These languages belong to a class of programming languages called logic programming languages, where computation is equated with deduction. The latter two languages above involve constraint satisfaction.
• Inductive logic programming (ILP) utilizes the concepts of logic programming together with methods of generalization to learn from examples. The products of ILP systems are programs that incorporate some features of the positive examples, avoiding the characteristics of the negative examples. Applications currently exist in areas as diverse as drug design, finite element analysis, and natural language understanding.

We also note the use of AD concepts and systems in research application systems, particularly in artificial intelligence and deductive databases.

General Observations

In addition to achievements, many characteristics of a field are important to understanding that field. Following are some major characteristics of the automated deduction field.

• Automated deduction is considerably more sophisticated and uses more diverse techniques than was the case just two decades ago.
• Applications are appearing, but they are selective. Many are in the areas where they were expected, but are of lower complexity than our visions of several decades ago.
• The themes common to all applications are to find methods to severely limit the proof search space and/or to limit the deductive component to lower complexity tasks. Lower complexity is a relative and dynamic term, in that the boundary of the practically achievable constantly moves upward.
• Open problems in mathematics have now been solved by using AD techniques and systems. Solutions have been found both in interactive mode and fully automatic mode, both by proof discovery and by counterexample production. The mathematical areas approachable to date have been algebraic or combinatoric in nature, with our capabilities in continuous mathematics well below the open problem realm at present.
• The high-intensity push to develop hardware and software verification systems in the 1970s and beyond showed our underestimation of the task difficulty. There are indications that, in reaction, funding in the United States subsequently has fallen below the optimal rate of investment. More productive is moderate but sustained funding over a long period of time.
• After the initial optimism wore off, the program synthesis area was viewed by many as a blue-sky area with little near-term payoff. A few notable projects have shown that applications are possible if carefully selected and given sustained support. Here the key is carefully constrained deduction requirements.
• Mathematics and logic education should profit from the work of the AD field. Successful educational products and even automated college courses already exist. There is much more potential than has been realized, but the realization will require cooperation with educators.

In addition to the cited general observations, the following specific observations can be made.

• Work on applications, particularly verification, adds to the core capabilities and hence our research base.
• Verification proofs are ``shallow and messy'', that is, more easily discovered than the mathematical proofs currently attempted but require a larger collection of proof methods. One consequence of the latter property is that the verification area leads in integration of different proof techniques within single systems.
• The incorporation of computer algebra systems will enhance significantly the proof capabilities in both the verification and mathematics areas.
• Much needs to be done to make AD systems more user friendly before they will be used as mathematical assistants. However, for most mathematicians the problem is not just lack of readable proofs but lack of reasoning power at the level that humans reason.
• A recurring dream is to build an archive of formally verified mathematical results that will include the entire core of mathematics. Use of AD systems would be needed to provide both the assurance of formal verification and the capability to handle the quantity of work.
• Areas as distinct from mathematics as economics and sociology can profit from use of formal methods to express and evaluate theories. Use includes testing consistency of a proposed theory extension with the core knowledge base and generating ramifications of a proposed extension.

Next are observations concerning resource use and availability. Regarding research resources, the United States has lost the role of major player in automated deduction.

• Research momentum is shifting to Europe as the funding in the AD field increases in Europe and decreases in the United States. (The U.S. decrease includes Defense Department funding of areas such as verification systems.) One measure of the shift is the recent dominance of the international Conference on Automated Deduction by European researchers.
• Research activity in Asia and Australia is growing and has already yielded significant research contributions.
• In the United States, the number of new researchers entering the field is close to zero. Reasons are the lack of government funding and the nonexistence of new university faculty positions in this area.

The AD systems, the resources of the user communities, are changing in nature and distribution.

• Some of the best AD systems are of U.S. origin, but the number of AD research systems is probably larger in Europe now.
• In the future there almost surely will be fewer top-ranked AD systems. The systems will be more complex, in centers with more researchers and support staff, and supplying on-site resources for visiting researchers. Stable (hence not leading-edge) versions of these systems will be available for distribution and as inference engines in application packages.

Recommendations

The recommendations given here do not fully coincide with those in the report body. Some appearing here are considered self-explanatory and are not expanded later. Some appear in the report body in contexts not easily summarized here. We present only the major recommendations in this summary.

For the Funding Agencies

• The key problems of this field are complex, and progress is generally incremental. Sufficient progress has been made to yield real-world applications, admittedly at the lower end of our original expectations. Building on the research of the past decades, new advances now are likely to yield some immediate payoff, but the large payoffs are accumulative.
  • Provide steady funding for basic research. This includes both AD system research and formal methods research.
  • Provide significant funding for deduction engineering. This is primarily AD system improvements, which in many cases involve sophisticated advances. Like other engineering disciplines, deduction engineering is a means, not a goal. However, its importance deserves special notice.
  • Set funding priorities for technical advancement consistent with the priorities suggested for the AD community at the end of this summary.
  • Provide support for the formalization of the core of mathematics when organizational and technical issues are in place for a meaningful attack on the task.

• Research and development within the application areas of AD enhance the core capabilities as well.
  • Provide funding for promising applications, both as venture capital for plausible projects and as maintenance funding for further development of prototype applications.
  • Provide sustained funding for mathematical proof systems, with some priority given to systems that tackle open problems of interest to the mathematics community.
  • Provide increased funding for basic research in formal verification methodology. This area contributes directly to AD core capability and hence to other applications, as well as to its own growing list of applications.
  • Fund both basic program synthesis research and application projects. Support processes that will help locate further applications.

• Because few researchers are entering the field, we must increase the efficiency of the existing researchers and those that do join the field.
  • Increase funding for postdoctoral students.
  • Provide funding for U.S. researchers to take sabbaticals at foreign AD centers.
  • Provide for grants to attend U.S. AD centers and to maintain connections to AD systems for remote computing.

• It is important to provide potential users with access to the technology of the field.
  • Provide funding for application workshops.
  • Provide funding for short courses at AD centers for potential users.

For the Universities

• Encourage the teaching of logic and formal methods to both mathematicians and computer scientists so that these professionals will understand the opportunities and methodologies associated with automated reasoning. Such opportunities will significantly increase over their working lifetimes.
• Encourage educators to work with AD practitioners to develop mathematics and logic courses using the tools of the AD field.

For Other Research Centers

• For centers housing major AD systems
  • Provide for researchers to reside for work periods and to have remote access to major AD systems.
  • Provide short courses on the use of the AD system(s), both for AD researchers who may then use and augment the system and for possible application users.

• For centers that have developed application systems
  • Provide workshops on the application technology, within proprietary and national security limits.
  • Explore possible working relations with appropriate AD research personnel for an in-house work period. Seek to educate the researcher on in-house technology needs.

For Industry

• Support continued research in formal verification methods.
• Support exploration of AD methods to enhance symbolic testing.
• If appropriate, offer the same opportunities suggested for research centers above.

For the AD Community

The recommendations for practitioners of automated deduction are broken into two categories: general and technical.

• General recommendations
  • Make AD systems accessible to nonspecialists. This includes input/output in the formalism of the user and output using natural language to report inference connections.
  • Develop a set of open problems in mathematics that have a reasonable axiomatic formulation and hence may be approached by AD methods. Maintain a Web site for the listing of such problems.
  • Identify a Grand Challenge problem whose major component uses AD technology. For maximum visibility and outside interest the problem should be both economically and intellectually important, although an appropriate open mathematical problem could be of sufficient stature to serve as a Grand Challenge problem.
  • Support the competition for AD systems held at recent AD conferences. Enlarge the competition categories so all major classes of AD systems are included. The purpose is more to ``improve the breed'' than to encourage publicity outside the field.
  • Offer short courses on major AD systems. Provide for apprenticeships and other means for interested professionals to learn the system operation in detail. Provide network accessibility for remote use of AD systems.

• Technical recommendations. Two levels of priority are offered; items are unordered within each list regarding priorities. This list is incomplete and must be augmented by the recommendations in the report body.
  • Make AD systems easier for nonexperts to use, including increased automation of interactive tasks.
  • Expand work on proof presentation, including natural language augmentation.
  • Find effective ways to use larger inference steps.
  • Develop effective ways of combining interactive and automatic search procedures.
  • Continue to integrate proof methods to form more composite systems.
  • Incorporate computer algebra systems into AD systems. This effort must include addressing some problems with correctness of computer algebra systems.
  • Continue priority attention to equational logic and the techniques, such as rewrite rules, that process the logic.
  • Continue priority attention to mathematical induction.
  • Accelerate work in proof planning, including proof abstraction and proof by analogy.
  • Provide more integration of model generation with proof finding.
  • Continue efforts to introduce ``semantics'' (problem-specific information not easily axiomatized) into AD proof guidance.

  The following technical recommendations are assigned a somewhat lower priority at this time although each may, or will, be very important at some point in the future.

  • Pursue methods for automated proof discovery applicable to the continuous mathematics domain. This problem domain is important because it includes a good portion of mathematics, but the methodology needed must include techniques quite different from any used to date in discrete mathematics. Good work has been done in this area but is rare, and without some breakthroughs we expect progress to be slow here. Interactive mathematical assistant systems should be encouraged for their own value and as the best vehicles for progress in this area.
  • Pursue AD systems for nonclassical logics. At present, temporal logic is important, and AD systems to better handle this class of logics would be welcome now.
  • Pursue parallel computation paradigms for deduction. Deduction is particularly suited for gains from parallelization, but big gains in parallelization will come eventually from outside the AD field, and work within the AD field on parallelization will be particularly effective then. The limited activity of implementing parallel versions of (portions of) leading AD systems may be appropriate now.
  • Give more attention to artificial intelligence, neural net, and general stochastic methodologies for application to proof guidance. In particular, explore the use of learning from past experience. Automated deduction capabilities will be always severely limited if capabilities associated with abstract pattern recognition and learning are not incorporated into proof guidance. Although such capabilities are vital to real progress, there is currently little idea how to achieve advances here. Funding should be selective but aggressive when real advances become feasible.