Nqthm

[1] The system was developed by Robert S. Boyer and J Strother Moore, professors of computer science at the University of Texas, Austin.

The function TIMES is part of the BOOT-STRAP (called a "satellite") and is defined to be The formulation of the theorem is also given in a Lisp-like syntax: Should the theorem prove to be true, it will be added to the knowledge basis of the system and can be used as a rewrite rule for future proofs.

There are macros for LaTeX that can transform the Lisp structure into more or less readable mathematical language.

This is a great help, as the system has an unproductive tendency to wander down infinite chains of inductive proofs.

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.