On this tour you will learn a little about what ACL2 is for rather than how ACL2 works. At the bottom of the ``page'' (which may extend beyond the end of your screen) there is a small ``flying tour'' icon. Click on it to go to the next page of the tour.
The tour visits the following topics sequentially.
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
We intend the tour to take about 10 minutes of your time. Some pages on the tour contain pointers to other documents. You need not follow these pointers to stay on the tour.
