The Boyer-Moore Theorem Prover (NQTHM)
The Boyer-Moore theorem prover started in Edinburgh, Scotland, in
1971. It was originally a fully-automatic theorem prover for a logic
based on a home-grown dialect of Pure Lisp. The key ideas in the
theorem prover were:
The design of our system was heavily influenced by John McCarthy and
- (1971) the use of Lisp as a working logic;
- (1971) the reliance on a principle of definition for total recursive
- (1971) the extensive use of rewriting and ``symbolic evaluation'' and
- (1971) an induction heuristic based the failure of symbolic evaluation.
Over the decades the theorem prover evolved considerably. The
most dramatic change occurred very early.
After this change, the system was no longer fully automatic:
the system's performance was and is determined by the user. The
informed user can lead the system to difficult proofs by the careful
selection of lemmas to prove. But the user cannot imperil the
soundness of the system.
- (1974) We programmed the simplifier to make use of rewrite rules
derived from previously proved lemmas.
For other important innovations to our theorem prover, click here. For a history of the mechanization of induction focused on the Boyer-Moore work
of the 1970s and early 1980s (Edinburgh Pure Lisp Theorem Prover and
NQTHM), see Automation of Mathematical Induction
as part of the History of Logic co-authored with C.P. Wirth.
Early critics focused on the practical irrelevance of proving theorems about
pure Lisp, since serious applications were not programmed in Lisp.
However, our view was that Lisp was a logic in which other systems could be
conveniently formalized. Because of this, our system found its most
interesting use in practical applications. Some of the correctness
results and theorems are suggested below.
I apologize to the many users whose favorite examples were left off this list.
- (1971) list concatenation
- (1973) insertion sort
- (1974) a binary adder
- (1976) an expression compiler for a stack machine
- (1978) uniqueness of prime factorizations
- (1983) invertibility of the RSA encryption algorithm
- (1984) unsolvability of the halting problem for Pure Lisp
- (1985) FM8501 microprocessor (Warren Hunt)
- (1986) Godel's incompleteness theorem (Shankar)
- (1988) CLI Stack (Bill Bevier, Warren Hunt, Matt Kaufmann, J Moore, Bill Young)
- (1990) Gauss' law of quadratic reciprocity (David Russinoff)
- (1992) Byzantine Generals and Clock Synchronization (Bevier and Young)
- (1993) bi-phase mark asynchronous communications protocol
- (1993) Motorola MC68020 and Berkeley C String Library (Yuan Yu)
- (1994) Paris-Harrington Ramsey Theorem (Ken Kunen)
For more details about Nqthm, PC-Nqthm, and the proofs done with them,
including proper bibliographic references for the work mentioned
Nqthm and PC-Nqthm are available for free via ftp. Sources and
documentation are included.