Major Section: ACL2-TUTORIAL
Beginning users may find these annotated scripts useful. We suggest that you read these in the following order:
Tutorial1-Towers-of-Hanoi Tutorial2-Eights-Problem Tutorial3-Phonebook-Example Tutorial4-Defun-Sk-Example Tutorial5-Miscellaneous-Examples
The page http://www.cs.utexas.edu/users/moore/publications/tutorial/rev3.html contains a script that illustrates how it feels to use The Method to prove an unusual list reverse function correct. The screen shots of ACL2's proof output are outdated -- in the version shown, ACL2 does not print Key Checkpoints, but the concept of key checkpoint is clear in the discussion and the behavior of the user.
At http://www.cs.utexas.edu/users/moore/publications/tutorial/kaufmann-TPHOLs08/index.html is the demo given by Matt Kaufmann at TPHOLs08, including all the scripts. There is a gzipped tar file containing the entire contents of the demos.
At http://www.cs.utexas.edu/users/moore/publications/tutorial/sort-equivalence is a
collection of scripts illustrating both high-level strategy and lower-level tactics dealing
with the functional equivalence of various list sorting algorithms. Start with the
README on that directory. There is also a gzipped tar file containing all the
scripts.
