The Boyer-Moore Theorem Prover (NQTHM)

• (1975?) A variety of ``rule classes'' were introduced, allowing previously proved theorems to control many aspects of the system's behavior. The system began evolving towards being a ``theorem proving shell'' with which one could fashion a prover for a particular domain.
• (1978?) An efficient representation of constants was introduced into the system, along with mechanisms for computing the values of axiomatically defined functions on such constants. The logic thus became efficiently executable and could be used as an applicative programming language. This important feature of Nqthm is still (1997) not widely appreciated.
• (1980?) ``Metafunctions'' were introduced, whereby hand-coded Lisp simplifiers could be proved correct and then incorporated into the system.
• (1982?) A linear arithmetic decision procedure was integrated into the simplification process, illustrating that decision procedures have their roles in the general-purpose setting but that their effective use is exceedingly difficult.
• (1985?) V&C$, an evaluator for the logic, was added to the logic by a novel means, allowing the formalization of partial-recursive functions.
• (1987) Matt Kaufmann implemented PC-Nqthm, giving Nqthm an interactive proof checking capability.
• (1990?) ``Functional instantiation'' was added as a derived rule of inference, giving our first-order logic some ``higher-order'' features.