Boyer's ftp directory

The subdirectory cli-notes contains a few members of the Internal Notes series of Computational Logic, Inc. These are exactly the internal notes referenced in the second edition of A Computational Logic Handbook.

The subdirectory cli-reports contains all of the reports of Computational Logic that were distributed by anonymous ftp through 1997. For an overview, see the file cli-reports/index.html

The subdirectory diss contains the Ph. D. dissertations of some of my former students.

The subdirectory fm9001 describes the FM9001 microprocessor designed, built, tested, and formally verified by Warren Hunt and Bishop Brock.

The subdirectory ics-reports provides many of the technical reports of the Institute for Computing Science and Computer Applications, University of Texas at Austin, 1978-1987.

The file gve.tar is the Gypsy Verification Environment, the work of Don Good (, Mike K. Smith, Rich Cohen and others. This utterly vast and wonderful project was begun at ICSCA at the University of Texas and further enhanced at Computational Logic.

The subdirectory pc-nqthm contains Matt Kaufmann's extensions to Nqthm.

The file pc-nqthm-1992.tar.Z contains Kaufmann's extensions to the Boyer-Moore prover.

The subdirectory nqthm contains the Boyer-Moore prover, a.k.a. Nqthm.

Not on this directory, but highly recommended is Gnu Common Lisp (GCL). See

See also Boyer's home page at