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 Woody Bledsoe.

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.

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.

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

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

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