From: boyer@CLI.COM (Robert S. Boyer)
Date: Fri, 15 Sep 95 09:35:29 CDT
Message-Id: <9509151435.AA13871@dilbert.cli.com>
To: qed@mcs.anl.gov
Subject: Announcing the Availability of More Nqthm-Checked Theorems
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


Below we describe how to obtain, install, and mechanically proof-check some
files containing Nqthm-checked theorems over and above those in the `examples'
directory distributed with Nqthm-1992.

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