These additional files include:
* Much of the `Clinc Stack'
a. The FM9001 microprocessor
(Brock & Hunt, with contributions from Kaufmann)
[fm9001-piton/fm9001-replay.events]
b. The Piton assembler (Moore)
[fm9001-piton/piton.events]
c. The `big-add' Piton example (Moore)
[fm9001-piton/big-add.events]
d. A Piton program that wins at Nim (Wilding)
[fm9001-piton/nim-piton.events]
* A Paris-Harrington Ramsey theorem (Kunen)
[kunen/paris-harrington.events]
* An illustration of the surprising power of EVAL$ (Kunen)
[kunen/induct.events] (surprising to Boyer and Moore anyway)
* The arithmetic-geometric mean theorem
(Kaufmann & Pecchiari)
[numbers/arithmetic-geometric-mean.events]
* The mutilated checkerboard theorem in the general NxN case
(Subramanian)
[subramanian/mutilated-checkerboard.events]
* A simple real-time system, the classic train example (Young)
[young/train.events]
* A theorem about coin tossing probabilities (Kaufmann)
[numbers/tossing.events]
* A proof of correctness of a real-time scheduling algorithm
(Wilding)
[numbers/scheduler.events]
Some documentation for some of the above proof efforts may be found as follows:
* FM9001 microprocessor http://www.cli.com/hardware/fm9001.html
* Piton assembler http://www.cli.com/reports/files/022.ps
* Nim playing program in Piton http://www.cli.com/reports/files/078.ps
* Paris-Harrington Ramsey http://www.cs.wisc.edu/~kunen/ramsey.ps
* EVAL$ http://www.cs.wisc.edu/~kunen/nqthm.ps
* Arithmetic-geometric mean http://www.cli.com/reports/files/100.ps
* Real time train http://www.cli.com/reports/files/093.ps
* Mutilated checker board
ftp://ftp.cli.com/pub/nqthm/nqthm-1992/examples/subramanian/mutilated-checkerboard.ps
* Real-time scheduling ftp://ftp.cli.com/home/wilding/scheduler-proof.ps
The source files for these theorems, named within square brackets above, may be
obtained individually from the directory
ftp://ftp.cli.com/pub/nqthm/nqthm-1992/examples/ or altogether in the single
file ftp://ftp.cli.com/pub/nqthm/nqthm-1992/1995-examples.tar.Z.
Also included on the tar file are new `driver' files for doing a replay of all
the examples under Nqthm-1992, both these new examples and those previously
distributed with Nqthm-1992. A Gnu Emacs TAGS file for all the event commands
in all the examples is also provided.
Supposing that one has obtained the file
ftp://ftp.cli.com/pub/nqthm/nqthm-1992/1995-examples.tar.Z, and assuming that
Nqthm-1992 has been installed, and resides in the directory `nqthm-1992',
proceed as follows:
1. Move the file `1995-examples.tar.Z' to the `nqthm-1992' directory.
2. % cd nqthm-1992
3. % uncompress 1995-examples.tar.Z
4. % tar xvf 1995-examples.tar
5. % rm 1995-examples.tar (optional, to save space)
Assuming that Nqthm-1992 has been installed correctly, it should now be
possible to execute the following command, when connected to the `nqthm-1992'
directory, to have all the new event files proof-checked by Nqthm-1992. This
checking process will take many hours on a contemporary work station.
6. % make giant-test
On operating systems not Unix related, instead of the previous command one may
load the files `examples/driver.lisp' and `examples/driver-sk.lisp' to recheck
the theorems. See the file examples/README for further details.
Bob Boyer and J Moore
September 1995
P. S. This message may also be found as the file
examples/README-for-1995-examples on the tar file mentioned above.
P. P. S. For information on obtaining the Nqthm prover itself, please see
ftp://ftp.cli.com/pub/nqthm/nqthm-1992/nqthm-1992.announcement