A Walking Tour of ACL2

On this tour you will learn a little more about the ACL2 logic, the theorem prover, and the user interface.

This time we will stick with really simple things, such as the associativity of list concatenation.

We assume you have taken the Flying Tour but that you did not necessarily follow all the ``off-tour'' links. So this tour may revisit some pages you've seen. Just click on the Walking Tour icon at the bottom of each page.

On this tour you will see many more links marked . We would like to discourage you from following these links right now. However we encourage you to note them. Basically, the sign here illustrates the documentation and introduces you to its main entry points. Once you have started to use ACL2 you can take the Walking Tour again but pursue more of the indicated links.