Major Section: ACL2 Documentation
This section contains a tutorial introduction to ACL2, some examples of the use of ACL2, and pointers to additional information.
If you are already familiar with Nqthm, see nqthm-to-acl2 for help in making the transition from Nqthm to ACL2.
If you would like more familiarity with Nqthm, we suggest CLI
Technical Report 100, which works through a non-trivial example. A
short version of that paper, which is entitled ``Interaction with
the Boyer-Moore Theorem Prover: A Tutorial Study Using the
Arithmetic-Geometric Mean Theorem,'' is to appear in the Journal of
Automated Reasoning's special issue on induction, probably in 1995
or 1996. Readers may well find that this paper indirectly imparts
useful information about the effective use of ACL2.