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:

(1971) the use of Lisp as a working logic;
(1971) the reliance on a principle of definition for total recursive functions;
(1971) the extensive use of rewriting and ``symbolic evaluation'' and
(1971) an induction heuristic based the failure of symbolic evaluation.

The design of our system was heavily influenced by John McCarthy and Woody Bledsoe.

Over the decades the theorem prover evolved considerably. The most dramatic change occurred very early.

(1974) We programmed the simplifier to make use of rewrite rules derived from previously proved lemmas.

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.

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.

(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)

I apologize to the many users whose favorite examples were left off this list.

For more details about Nqthm, PC-Nqthm, and the proofs done with them, including proper bibliographic references for the work mentioned above, see

The Boyer-Moore Theorem Prover and Its Interactive Enhancement, with M. Kaufmann and R. S. Boyer, Computers and Mathematics with Applications, 29(2), 1995, pp. 27-62.

Nqthm and PC-Nqthm are available for free via ftp. Sources and documentation are included.

[Best Ideas] [Publications] [Research] [Home]