|
|
|---|
|
|
|
|---|
The Tours
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
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
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 ACL2 User's 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 browser'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.
If you take the tours in a text-based format (such as using the :DOC command in Emacs), they will probably be unsatisfying because we use gif files and assume you can navigate ``back.''