We make no attempt to be historically complete, but rather to note events of particular pertinence to our present status. We do note the first automated theorem prover, the Logic Theorist developed by Newell, Shaw, and Simon in the mid-1950s [81]. The Logic Theorist was significant for several innovations, including the first use of linked lists and its use of human problem-solving techniques to solve reasoning problems in logic. This approach to proving logic theorems drew a reaction from several logicians, such as Paul Gilmore, Hao Wang, and Martin Davis. They felt (correctly) that better results in proving theorems could be realized immediately by using tools of mathematical logic rather than being restrained to the imitation of humans.
One of the proof procedures that followed the Logic Theorist was the Davis-Putnam procedure [34] [33]. This procedure is a propositional decision procedure when provided a fixed propositional formula but is also a first-order logic proof procedure whenever larger propositional formulas are formed in a standard way from the given first-order formula. Although the later resolution proof method formalized a generally better way of relating propositional formulas and first-order formulas, the propositional decision procedure is receiving as much attention today as when first presented. (There are actually two related procedures with the same general label; compare the two above referenced papers or see, e.g., [36].) The Davis-Putnam procedure has been used recently in the mathematics realm to solve some open problems in quasigroups [94] and in the artificial intelligence realm as a method to solve constraint satisfaction problems [35] [36].
Another important program developed in the 1950s was the Geometry Theorem Proving Machine, a project headed by Gelernter at IBM [42] [43]. This program used a geometry diagram as semantic information to prune the search tree sufficiently to prove many results that high-school students prove on final exams. This use of problem-specific information, called the semantics of the problem, is one of the biggest challenges in automated deduction. The ability to prove interesting theorems in geometry and give readable proofs has been surpassed only recently by Chou, Gao, and Zhang in automated theorem provers using the area method perfected by Zhang [22]. We say more on this later.
The resolution proof method introduced by J. A. Robinson [92] was a significant advance over preceding proof procedures for its introduction of the unification algorithm that provided a provably complete method for working at the first-order level; the Herbrand terms did not have to be enumerated. The simplicity of the inference rules and the later discovery of how to retrieve ``answers'' from the substitutions made in the proof process led to its inclusion in many programs, from the ML programming language system (polymorphic type inference) to natural language processors, question-answering systems, explanation-based reasoners, and deductive database systems. The inference engine of the logic programming language Prolog is a resolution system. The resolution calculus has been at the heart of several successful theorem provers developed at Argonne National Laboratory, of which the latest is the theorem prover Otter developed by McCune [70]. Otter is currently being used by mathematicians in research published in standard mathematics journals, has been used to solve several open mathematics problems, and has been used in ways only indirectly related to mathematical theorem proving, such as circuit design and verification.
An important contribution of the AD community was introduced under the name demodulation by Wos and G. Robinson at Argonne [108]. It is an equational inference rule, and later developed into the subdiscipline of term rewriting, pushed forward substantially by the paper of Knuth and Bendix [59]. Term rewriting is used in most of the AD systems that we discuss in this report and is used in computer algebra systems and functional language implementations.
One success story for the application of automated deduction (AD) concepts and tools is the logic programming area. The most famous example is Prolog, which contains a resolution-based inference engine at its core [93] [16]. (Historically, the deduction mechanism of Prolog is a merger of resolution and a related procedure called Model Elimination [60].) Prolog is one of the two major AI languages, predominating in Europe (whereas LISP is dominant in the U.S.). It was instrumental in the implementation of many of the early backchaining expert systems and is used extensively as a prototyping language for many process designs, among other uses. Two applications conferences are currently held each year, one in Europe and one in Japan. More recently logic programming technology has been combined with constraint solving to create the important concept of constraint logic programming and the realization of immensely useful constraint logic programmming systems. Other languages based on deduction include ML [76] and Lambda-Prolog [80]. The former is becoming an influential language for type inference, among other things, and the latter is used to prototype theorem provers.