The Boyer-Moore Theorem Prover (NQTHM)
The dates below are only approximate.
- (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.
V&C$, an evaluator for the logic, was added to the
logic by a novel means, allowing the formalization of partial-recursive
- (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''