A Few CLI Internal Notes
This directory contains several members of the Internal Notes series of
Computational Logic, Inc. These include the internal notes referenced in the
second edition of A Computational Logic Handbook. pdf versions of
these ps files are also available here.
W. R. Bevier, A Library for Hardware Verification,
M. Kaufmann, An Example in Nqthm: Ramsey's Theorem, 1991.
Bishop Brock, An Experimental Implementation of Equivalence Reasoning in the
Boyer-Moore Prover, 1988.
M. Kaufmann, An Integer Library for Nqthm, 1990.
M. Kaufmann, An Instructive Example for Beginning Users of the Boyer-Moore Theorem Prover, 1990.
W. D. Young, A Simple Expression Compiler: A Programming and Proof
Example for an Nqthm Course, 1990.
M. Kaufmann, A Simple Example for Nqthm: Modeling Locking, 1991.
John R. Cowles, Using NQTHM to Verify Insert, Search, and Traversal
Functions for Search Trees, 1991.
John R. Cowles, Meeting a Challenge of Knuth, 1991.