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.

- i ii o on the Gilbreath Card Trick
- i ii o on asynchronous communication and the biphase mark communications protocol
- i ii o the binomial theorem
- i ii o on a controller
- i ii o on Fibonacci numbers
- i ii o illustrations of the use of constrained functions and functional instantiation
- i ii o quadratic reciprocity
- i ii o another proof of quadratic reciprocity
- i ii o on the syntax of the Nqthm extended logic
- i ii o on Ackermann's original function and R. Peter's version of it
- i ii o the existence of nonprimitive recursive functions
- i ii o elementary list processing, number theory through Euclid's gcd theorem and prime factorization, the soundness and completeness of a tautology checker, the correctness of a metafunction, the correctness of a simple assembly language program, and the correctness of a simple optimizing expression compiler
- i ii o on the 91 function
- i ii o the invertibility of the Rivest/Shamir/Adleman public key encryption algorithm
- i ii o on operational semantics
- i ii o on tic-tac-toe
- i ii o the Turing completeness of Pure Lisp
- i ii o the unsolvability of the halting problem for Pure Lisp
- i ii o Wilson's theorem
- i ii o the termination of Takeuchi's function
- i ii o on a simple separation kernel
- i ii o on string-functional semantics for circuit descriptions
- i ii o an introduction to Nqthm
- i ii o on sequences and Nqthm's shell principle
- i ii o on a compiler and runtime system for a subset of the Nqthm language
- i ii o on a garbage collector
- i ii o the correctness of a Piton program for adding arbitrarily long numbers
- i ii o the correctness of the gate-level implementation of the FM9001 microprocessor
- i ii o on a Nim playing program in Piton for the FM9001
- i ii o on the implementation of Piton for the FM9001
- i ii o on a Fortran implementation of a string searching algorithm
- i ii o on a Fortran implementation a square root algorithm
- i ii o on a Fortran implementation of a linear-time majority vote algorithm
- i ii o formalizations of the machine code for the 16-bit FM8501 microprocessor, a register transfer model of a microcoded implementation of the machine, and a proof of their correspondence
- i ii o on a simple expression compiler
- i ii o on the permutation-independence of list processing functions
- i ii o on a generalization algorithm
- i ii o on Koenig's tree lemma
- i ii o a model of a simple data base against which read and write transactions can occur
- i ii o the correctness of a merge sort function
- i ii o Ramsey's theorem for exponent 2
- i ii o on handling partial functions with Nqthm
- i ii o on the notion of permutation via bags
- i ii o Ramsey's theorem for the infinite case
- i ii o on the rotations of lists, intended as an introduction to Nqthm
- i ii o an exercise in reverse Polish notation evaluation
- i ii o on the Gilbreath Card Trick
- i ii o on Ackermann's function
- i ii o on induction and the nonconstructiveness of Nqthm-1992
- i ii o on the fundamental theorem of arithmetic
- i ii o the Paris-Harrington Ramsey theorem
- i ii o the arithmetic-geometric mean theorem
- i ii o on bags
- i ii o Matijasevich's lemma about Fibonacci numbers
- i ii o on the integers
- i ii o on the natural numbers
- i ii o on the game Nim
- i ii o on the optimality of an earliest-deadline-first scheduler
- i ii o on coin tossing
- i ii o the Church-Rosser theorem
- i ii o Goedel's incompleteness theorem
- i ii o on tautologies
- i ii o on the mutilated checkerboard problem
- i ii o on a mutual exclusion algorithm
- i ii o on a mutual exclusion algorithm
- i ii o on a controller
- i ii o on machine code that finds the maximum value in an integer array
- i ii o on machine code produced by assembly code embedded in C
- i ii o on machine code for binary search
- i ii o on machine code for 21 of the 22 C String library functions
- i ii o on machine code for gcd
- i ii o on machine code produced for using C function pointers
- i ii o on machine code for gcd
- i ii o on machine code produced for C function calls
- i ii o two theorems in finite group theory, including Lagrange's theorem
- i ii o on machine code for Newton's square root algorithm
- i ii o on machine code produced from Ada
- i ii o on machine code for computing integer logarithms
- i ii o a formal specification of about 80% of the user available instructions for the Motorola MC68020 microprocessor
- i ii o definitions and lemmas about the formalization of the MC68020
- i ii o on machine code for a linear time majority vote algorithm written in C
- i ii o on machine code for Quick Sort
- i ii o on machine code for the C switch statement
- i ii o on machine code for zeroing an array