We present here a brief, and very informal, introduction to ACL2. Our purpose is to provide just enough ACL2 background to support reading the ACL2 formulas displayed in this book's case studies. The reader interested in learning more about ACL2 is invited to take a look at the companion volume, , and to visit the ACL2 home page (see page 4).
KeywordsBinary Tree Companion Volume Proof Obligation Recursive Definition Empty List
Unable to display preview. Download preview PDF.