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

• 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