A Flying Tour of ACL2

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'' (which may extend beyond the end of your screen) there is a small ``flying tour'' icon. Click on either icon 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
     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.