Some Examples of Nqthm-1992 Use

The following list of uses of Nqthm-1992 is based upon Chapter 14 of A Computational Logic Handbook, Boyer and Moore, Second Edition, Academic Press, 1998. See that chapter for further information about these examples, including who did the work and other citations.

Below, an i link gets the input, an ii link gets the input in a more traditional notation, and an o link gets the proof output.