CS 8803 Computational Logic
Spring 2006

Homework 3, Due 2/23/2006

• Read chapter 3 of CAR and do exercises 3.3,3.4, 3.11, and 3.18-3.22.
• Read chapter 4 of CAR and do exercises 4.6, 4.11, and 4.15-4.18.
• Read chapter 5 of CAR and do exercises 5.1-5.5, and 5.7.

Solutions should be checked using ACL2 and sent to Daniel Vogh via email gtg894a@mail.gatech.edu (and cc me, Pete). Recall that late homeworks will not be accepted.

You can work alone or in pairs. If you work with someone else, please do the programming together and do not simply split up the exercises amongst yourselves.

The Eclipse version of ACL2 should be downloaded and used in programming mode; see the tools page. Read appendix A of CAR (Computer-Aided Reasoning) for information on using the ACL2 system. You might want to skim appendix B.

Last modified: Fri Mar 17 09:47:30 EST 2006