ACL2 is a very large, multipurpose system. You can use it as a programming language, a specification language, a modeling language, a formal mathematical logic, or a semi-automatic theorem prover, just to name its most common uses. It has been used on a number of industrial applications. If you're uncertain as to whether your project is appropriate for ACL2 we urge you to look over this list or contact the ACL2 developers.
This home page includes all of ACL2's online documentation, which is quite extensive (over 4 megabytes). To help ease your introduction to ACL2, we have built two tours through this documentation.
If you are familiar with at least some of the industrial applications of ACL2, then you will understand the distance between the simple examples we talk about in these tours and the kinds of things ACL2 users do with the system.
Newcomers to ACL2 should first take the ``Flying Tour.'' Then, if you want to know more, take the ``Walking Tour.'' On your first reading, follow the two Tours linearly, clicking only on the icon of the Tour you're on. Beware of other links, which might jump you from one tour to the other or into the reference manual! Once you've had a coherent overview of the system, you might quickly repeat both Tours to see if there are unvisited links you're interested in, using your brower's Back Button to return to your starting points.
If after all this you want to learn how to use the theorem prover (!), see introduction-to-the-theorem-prover.
To start a tour, click on the appropriate icon below.
For readers using our :DOC or our TexInfo format in Emacs: The tours will probably be unsatisfying because we use gif files and assume you can navigate ``back.''
