ACL2-TUTORIAL

Parent topic:  Home

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

• INTRODUCTION -- introduction to ACL2

• STARTUP -- How to start using ACL2; the ACL2 command loop

• TIDBITS -- some basic hints for using ACL2

• TIPS -- some hints for using the ACL2 prover

• TUTORIAL-EXAMPLES -- examples of ACL2 usage

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.