Princeton University
Computer Science Dept.

Computer Science 496
Automated Theorem Proving

Andrew W. Appel

Spring 2001


Assignment 6

Prove the theorems on pages 166-167 of Huth and Ryan. (If you install the files described in Computation Tree Logic in Twelf, you can just fill in the holes in the as6.elf file.