R. S. Boyer and J S. Moore, A
Computational Logic Handbook, Second Edition, Academic Press, New
York, 1997.
Relevance: Nqthm user's manual
This book is the “final” user's manual for Nqthm. It was written about 8 years after the ACL2 project was started, by which time ACL2 had gained a sizeable user community despite the fact that Nqthm was still being used by some students and industrial researchers.