tutorial introduction to ACL2
Major Section:  ACL2 Documentation

This section contains a tutorial introduction to ACL2, some examples of the use of ACL2, and pointers to additional information.

You might also find CLI Technical Report 101 helpful for a high-level view of the design goals of ACL2.

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.