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 because we encouraged you not to. With the
Walking Tour we encourage you to visit off-tour links — provided they
are not marked with the tiny warning sign (

When you get to the end of the tour we'll give you a chance to repeat quickly both the Flying and the Walking Tours to visit any off-tour links still of interest.