step of the scheme. The above induction scheme produces the following two new conjectures: Case 2. (IMPLIES (ZEROP X) (EQUAL (TIMES X Z) (TIMES Z X))). and after winding itself through a number of induction proofs, finally concludes that Case 1. (IMPLIES (AND (NOT (ZEROP Z)) (EQUAL 0 (TIMES (SUB1 Z) 0))) (EQUAL 0 (TIMES Z 0))). This simplifies, expanding the definitions of ZEROP, TIMES, PLUS, and EQUAL, to: T. That finishes the proof of *1.1, which also finishes the proof of *1. Q.E.D. [ 0.0 1.2 0.5 ] COMMUTATIVITY-OF-TIMES Proofs Many proofs have been done or confirmed with the system, particularly (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) Gödel'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) (1992) A compiler for a subset of the Nqthm language (Arthur Flatau) (1993) bi-phase mark asynchronous communications protocol (1993) Motorola MC68020 and Berkeley C String Library (Yuan Yu) (1994) Paris–Harrington Ramsey theorem (Kenneth Kunen) (1996) The equivalence of NFSA and DFSA (Debora Weber-Wulff) PC-Nqthm A more powerful version, called PC-Nqthm (Proof-checker Nqthm) was developed by Matt Kaufmann. This gave the proof tools that the system uses automatically to the user, so that more guidance can be given to the proof. This is a great help, as the system has an unproductive tendency to wander down infinite chains of inductive proofs. Literature A Computational Logic Handbook, R.S. Boyer and J S. Moore, Academic Press (2nd Edition), 1997. 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. Awards In 2005 Robert S. Boyer, Matt Kaufmann, and J Strother Moore received the ACM Software System Award for their work on the Nqthm theorem prover. References External links The Automated Reasoning System, Nqthm The Boyer-Moore Theorem Prover (NQTHM) Even though the system is no longer being supported, it is still available at Runnable version on GitHub: Theorem proving software systems Common Lisp (programming language) software