Introduction to Some ACL2 Features

This introduction is an outline of a talk intended for those already familiar with ACL2, who would like to be further exposed to the range of features that it offers.

Note: In case you want to return to this introduction, you'll find a link to it by following the "[Tours]" link on the ACL2 home page and going to the end of the page to which it takes you.

This "laundry list" is intended to raise awareness of various ACL2 features that can be learned about in the documentation and/or by asking us. I plan to run through this outline VERY quickly (I realize that it's a very long list). Please let me know when you want me to elaborate a bit more (or less!). Then as time permits, I plan to summarize the following demo, accessible as the "fourth" demo after following the [demos] link on the ACL2 home page: 

http://www.cs.utexas.edu/users/moore/publications/tutorial/sort-equivalence/

NOTE: Please feel free to ask questions and to suggest where I should (or shouldn't) go into more detail. This outline is just a suggestion!

Outline

General

Automating proof control

Proof debugging tools

Other