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