*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 (dgatx@earthlink.net), 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
[[ftp://ftp.ma.utexas.edu/pub/gcl/README]].

See also Boyer's home page at [[http://www.cs.utexas.edu/users/boyer]].