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.
This home page includes all of ACL2's online documentation, which is quite extensive. To help ease your introduction to ACL2, we have built two tours through this documentation.
Newcomers to ACL2 should first take the ``Flying Tour.'' Then, if you want to know more, take the ``Walking Tour.''
To start a tour, click on the appropriate icon below.
For readers using Web browsers: This ``page'' actually contains many other pages of our documentation, organized alphabetically and separated by many blank lines. Be careful when using the scroll bar!
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.''
