Princeton University
Computer Science Department

Computer Science 598A
Automated Theorem Proving

Andrew Appel

Assignment 1
Spring 2003

General Information | Schedule | Assignments | Announcements
Assignment 1: Propositional Logic
  1. Exercises 1.3, page 12 of Huth and Ryan.
  2. Exercises 1.6.1 and 1.6.2, pages 36-37 of Huth and Ryan.
  3. Exercise 1.10.2, page 61 of Huth and Ryan.
  4. Use the Twelf logical framework to machine-check four simple proofs.
    1. Install Twelf 1.4 (or use it on the CS department servers).
    2. Copy the three files logic.elf, sources.cfg, and as1.elf, into a directory.
    3. Fill in the blanks of as1.elf until the proofs check successfully.
    4. Submit through the web.