CS 8803 Computational Logic
Spring 2005

Homework 3, Due 3/28/2005 before class starts

• 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 me via email. 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.

ACL2 is available locally; 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.