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.