pub/nqthm/nqthm-1992 The newest version of the theorem prover pub/pc-nqthm/pc-nqthm-1992 The newest version of the proof checker pub/nqthm-users-archive Archive of the users group pub/nqthm/nqthm-1992-images Images for sparc, Macintosh, Linux/486/GCL,...
The theorem prover is distributed under a license agreement found in the file ``basis.lisp.'' A Lisp compiler necessary for building the prover is also available at this site, GCL (Gnu Common Lisp) in pub/gcl/gcl-?.?.tgz, where ? is a version number. GCL is also available on Free Software Foundation CD-ROMS. Most importantly, no registration of any form is required for GCL, which is distributed under a Gnu license.
A World Wide Web home page is offered by Computational Logic at http://www.cli.com. Computational Logic, Inc, Austin, TX, USA is a company that Boyer and Moore founded together with Don Good that does many types of work in the verification field.