On this tour you will learn a little about what ACL2 is for rather than how ACL2 works. At the top and bottom bottom of the ``page'' there are ``flying tour'' icons. Click on either icon to go to the next page of the tour.
The tour visits the following topics sequentially. But on your first reading, don't navigate through the tour by clicking on these links; they are shown as live links only so that later you can determine what you've visited. Instead, just use the flying tour icons.
The Flight Plan
* This Documentation
* What is ACL2?
* Mathematical Logic
* Mechanical Theorem Proving
* Mathematical Models in General
* Mathematical Models of Computing Machines
Formalizing Models
Running Models
Symbolic Execution of Models
Proving Theorems about Models
* Requirements of ACL2
The User's Skills
Training
Host System
On your first reading, don't explore other links you see in the tour. Some of them lead to the Walking Tour, which you can take coherently when you finish this tour. Others lead into the extensive hyptertext documentation and you are liable to get lost there unless you're trying to answer a specific question. We intend the tour to take about 10 minutes of your time.
