Princeton University
Computer Science Department

Computer Science 598A
Automated Theorem Proving

Andrew Appel

Assignment 2
Spring 2003

General Information | Schedule | Assignments | Announcements
Assignment 2: Predicate Logic
  1. Exercise 1.11.13, page 68 of Huth and Ryan.
  2. Exercise 2.2.2, page 101 of Huth and Ryan.
  3. Prove some things using Twelf.
    1. Copy these Twelf files (they differ from those of assignment 1, in that the logic has existential and universal quantifiers): logic.elf, sources.cfg, as2.elf.
    2. Prove the four derived rules (found on page 31 of Huth & Ryan) using Twelf: mt, not_not_i, raa, and lem.
  4. Use Twelf to state and check proofs of Exercise 2.5.4, p. 126 of H&R.
  5. Use Twelf to do Exercise 2.5.6, p. 126-127.
  6. Use Twelf to do Exercise 2.5.9, p. 126-127.
Put all your Twelf proofs in the same file, as2.elf, and submit electronically.