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

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.

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)

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]