Major Accomplishments

Automated deduction has been an active area of research since the 1950s. (For a historical and sociological view of the field, see [72]. For an overview of the first twenty-five years of the field see [65]; see [95] for a comprehensive collection of the ``classic'' papers of 1957-1970.) Significant work has been done both in the early years and lately. Early important work includes the Davis-Putnam procedure and the resolution proof calculus. For recent notable work we focus on some significant theorem-proving systems: the geometry theorem provers of Chou et al. [21][22]; the Boyer-Moore interactive theorem prover Nqthm [14] and its successor ACL2 [55]; the Rewrite Rule Laboratory (RRL) of Kapur [54]; the resolution prover Otter [73][70] and the equational logic prover EQP [71] by McCune of Argonne National Laboratory; the interactive higher-order logic provers Nuprl (Constable, Cornell) [26], PVS (Shankar et al., SRI International) [84], and HOL (Gordon, Cambridge) [45]; and Analytica (Clarke et al., Carnegie-Mellon) [24], which embeds a symbolic computation program, Mathematica.$\!\!\!$  We briefly discuss in the following subsections some of the successes realized with use of these and other procedures and systems. We mention here just one recent and significant success: the discovery by the theorem prover EQP of a proof of an important mathematical conjecture. Settling the open problem, known as the Robbins algebra problem, is a milestone because it is by far the most difficult open problem to date whose proof was discovered by a computer (not just using a computer). This problem had been attempted by many mathematicians, including the famous logician Tarski, who subsequently directed a number of young mathematicians to it as a challenge problem. (The accomplishment by EQP, and McCune, was featured by the New York Times in December 1996 [82].) In the remainder of this section we review quickly some major achievements--both early and more recent-in automated deduction; such accomplishments lay the foundation for understanding the opportunities that we see ahead and the future directions we emphasize.