CS 8803 Computational Logic
Spring 2007

Homework 3, Due 2/21/2007

• 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 ACL2s and sent to Hwa-You Hsu via email hhsu3@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.

ACL2s 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 Feb 16 16:40:37 EST 2007