Read chapters 1-7 of CAR.
Do the exercises in chapters 3-6 that seem non-obvious. I am not going to collect solutions (for these exercises). Here are some suggested exercises for chapters 3-5.
You should use ACL2s. Instructions on how to use ACL2s will be sent shortly. You should download and use it in programming mode for the above exercises. You may want to refer to appendicies A and B of CAR (Computer-Aided Reasoning).
Do all the exercises in chapter 7 with paper and pencil (i.e.,
don't use ACL2s). In addition to collecting your homework, you
will be expected to present the solutions to the chapter 7
exercises on the board in class. Remember these are paper and
pencil proofs.
Last modified: Wed Nov 7 15:23:59 EST 2007