The recent achievements we name are programs because the recent advances that are conceptual are usually embedded in systems. We will discuss some of these achievements in more detail later. We will consider the more recent achievements in the context of a problem area.
Program synthesis is the perfect real-world, economically important application for automated deduction. But program synthesis, like most tasks requiring an automated intellect, is much further from reality than expected by optimists forty years ago (cf. the artificial intelligence world). Logic programming is in theory program synthesis, but in practice has too heavy a procedural component and too limited an area of effective application at present to be the final solution. For program synthesis the present secret to realizing applications is to greatly constrain the task that the AD machinery has to do. This key idea of constraining search applies in many areas where AD is applicable. There have been some notable successes, of which we note two of the best here. One is the KIDS system by D. Smith at Kestrel Institute [96], which provides algorithmic schema, such as divide-and-conquer and other search algorithm schema, within which a theorem prover operates. Success has been most dramatic in the scheduling algorithm area, where some derived scheduling algorithms have greatly outperformed the currently used algorithms. Another program synthesis success is the AMPHION project [97], sponsored by NASA and developed by Lowry and colleagues. The program provides astronomical calculations for satellite guidance. A theorem prover is used to glue together appropriate routines from a subroutine library, by matching specifications of each routine with specifications of the current demands.
Since programs will be written by humans for long time to come, program verification is clearly a very obvious and attractive goal. Considerable funds and effort were invested in program verification in the 1970s without commercial success. This situation has led to a considerable scaling back of expectations and investment in program verification and a shift of attention to hardware verification. In hardware verification the state of the art is approaching real-world systems, although the time required to accomplish the verification is not close to the needs of industry. An advantage of attention to hardware verification is that the verification of one process (a microchip) can safeguard a $100 million investment. (Such high-investment projects exist in software also, but such systems usually are so complex that formal verification for them is rare.) The ACL2 prover [55], the successor of Nqthm, recently was used interactively to obtain a formal proof of the correctness of the floating-point divide code for AMD's newest Pentium-like microprocessor. By ``interactively'' we mean the interaction of machine and human where (in this case) the human provides some search guidance and supplies key ideas the program cannot find on its own, such as difficult induction hypotheses and key lemmas. The verification was done at a very detailed level and is an impressive analysis. Analytica, developed at CMU by Clarke and Zhao [24], has just recently produced fully automatically a proof of the correctness of a division circuit that implements the floating-point IEEE standard. The prover is built around the symbolic computation system Mathematica. This exciting accomplishment does not void the work mentioned above, since the analysis is less detailed than the interactive verifications. The HyTech system developed at Cornell and Berkeley is a reasoning system for analysis of hybrid systems, primarily a symbolic model checker. Earlier versions of the system were built on top of Mathematica [46].
Other specification/verification systems exist that handle commercial problems. HOL [45], an interactive prover developed at Cambridge University and now being used and upgraded in industry, has produced several large correctness proofs of real security systems, delivered to customers. In another application, AT&T is using HOL to analyze and secure its large switching net. Lucent Technologies (Bell Labs) is using a combination of HOL and Nuprl to verify the SCI cache coherency protocol. The RRL system of Kapur and others has verified commercial-size adder and multiplier circuits [53].
At present, the AD technology most widely used in industry is in the realm of hardware verification. Such methods typically involve a representation for propositional formulas called Binary Decision Diagrams (BDDs) [77]. BDD manipulation procedures can perform the same task, determining a tautology or its negation, as do the Davis-Putnam procedure and propositional resolution procedures. However, they have been found particularly useful for circuit representation. BDD packages (for creation and combining of BDDs) are used in ``logic checkers'' that check the equivalence of two logic circuit designs.
BDD packages are often also used in model checking, where specifications, presented as propositional temporal logic formulas, are checked in the intended model, the circuit, presented as a state-transition diagram [23] [20]. Checking only one model, instead of all models, as theorem provers do, allows special-purpose algorithms to verify properties of moderately sized circuits fully automatically. IBM, Intel, and Motorola are among the companies that use model checking to verify specifications of microcontrollers. (Microcontrollers are integrated circuits, usually smaller than microprocessors, that make possible the ``intelligent'' appliances we have today.)
Besides logic checkers and model checkers, other BDD-based techniques are used for formal verification in industry. Of particular note is the symbolic trajectory evaluation method developed by Bryant and others [10].
As suggested above, for software verification progress is much slower; the objects being handled are more complex than hardware structures. However, recently there have been real-world applications of software verification [58]. Multiple examples exist in the areas of networks, transaction systems, and safety critical systems. The general area of concurrent systems is appropriate for formal verification with today's technology because the complexity overwhelms human capabilities but is relatively low compared with microprocessors. Sufficient success is seen in these areas that formal methods are receiving renewed attention by funding agencies. This attention to formal methods is much broader than AD technology, but some of the other techniques, such as symbolic testing, do use AD concepts and methodologies. The ability to tackle these real-world problems is primarily due to the improved capabilities of interactive systems such as Nqthm, ACL2, PVS, Nuprl, HOL, Coq (Huet, INRIA) [28], and Isabelle (Paulson, Cambridge) [86]. (These systems also are used for other purposes than verification.)
An anecdote underscores the economic and service value of validation of systems and specifications. A subsidiary of a German aircraft company was hired to produce software to control the switching of a complex broadcast network for the main German television company. The first submitted program failed to function properly, as did the second attempt. Under threat of a lawsuit by the television company, among other actions taken the producing subsidiary turned to the German research center DFKI for help. The software tool VSE (Verification Support Environment) developed in Germany, in part by DFKI, was used to respecify and verify an essential component of the system. In the process it was discovered that the original specifications for the network software given to the aircraft subsidiary were in fact inconsistent! Plans for the court case included calling the theorem prover as a witness but by then the parties had settled out of court. The first opportunity for AD software to get expert witness status was lost.
As for success in the mathematics realm, we have already mentioned
the settling of an important mathematical conjecture by a computer
using general proof discovery techniques under consideration
here. The field of mathematics is influenced in other ways by
automated deduction systems and methods. Some mathematicians are
using automated deduction programs as mathematical assistants to
achieve new mathematics. Ken Kunen, a University of Wisconsin
mathematician, has used Otter to prove several results concerning
quasigroups that have been published in the Journal of Algebra,
a traditional mathematics journal [61] [62].
(A quasigroup is a binary system 
whose multiplication
table is a Latin square.) Another paper on finding proofs of
quasigroup problems interactively, by Fujita, Slaney, and Bennett
(the last author a leading mathematician in this area), won a (shared)
Publisher's Prize (best paper award) at IJCAI (1993),
the leading international AI conference, as a recognition of the
significant work done [40]. In this paper a forward-reasoning
model generation system built at ICOT (Japan) was used. Otter has
been used to settle other open problems, such as finding minimal
axiom sets [69]. Work is not limited to first-order logic
and propositional logic provers. Nuprl (Constable et al.) helped
confirm two conjectures,
Higman's lemma [27] and Gerard's paradox [79][27],
that were under active investigation by humans at the time.
(For Higman's lemma, the humans won, but a subsequent machine-aided
proof showed that the original design for the proof method,
which the humans had abandoned, was indeed a feasible method of
proof.) The remarkable geometry provers developed by Chou, Gao,
and Zhang have been used to obtain new mathematical results in
non-Euclidean geometry.
Mathematics and logic education is a natural application for automated deduction. Some success stories already exist, and there are new opportunities in the form of inference systems potentially useful in education. Of note was an early application of AD in the completely computerized course in elementary logic at Stanford designed by Patrick Suppes (1960s). He followed that by a course in axiomatic set theory (1970s) [99]. Both embedded interactive theorem provers, with the student providing the major steps through a proof (usually with hints) and the theorem prover handling the details. The most sophisticated new systems are the geometry provers of Chou, Gao, and Zhang already mentioned. These systems can prove almost any theorem in rectilinear planar geometry (plus circles), Euclidean or non-Euclidean. Proofs for the standard theorems are usually short and elegant, with very readable proofs as output. Admittedly, this is not the same as having the provers embedded into a course structure, but the opportunity is there.
The above examples establish that there indeed have been many accomplishments in the field of automated deduction. With this as background we now explore the most promising future directions for research in this field.