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.

  • 57 W. R. Bevier, A Library for Hardware Verification, 1988.

  • 100 M. Kaufmann, An Example in Nqthm: Ramsey's Theorem, 1991.

  • 104 Bishop Brock, An Experimental Implementation of Equivalence Reasoning in the Boyer-Moore Prover, 1988.

  • 182 M. Kaufmann, An Integer Library for Nqthm, 1990.

  • 185 M. Kaufmann, An Instructive Example for Beginning Users of the Boyer-Moore Theorem Prover, 1990.

  • 210 W. D. Young, A Simple Expression Compiler: A Programming and Proof Example for an Nqthm Course, 1990.

  • 216 M. Kaufmann, A Simple Example for Nqthm: Modeling Locking, 1991.

  • 241 John R. Cowles, Using NQTHM to Verify Insert, Search, and Traversal Functions for Search Trees, 1991.

  • 286 John R. Cowles, Meeting a Challenge of Knuth, 1991.

    Main page.