Princeton University Computer Science Dept.

Computer Science 496 Automated Theorem Proving Andrew W. Appel

Spring 2001

Now, prove the formulas spec1 and spec2 in the file minsum.elf. These are the proofs of partial correctness of the minimal-sum section from Huth and Ryan, Section 4.3.3.

Keep your proof readable. One way to do this is to make appropriate lemmas. Another way is to label these lemmas with comments relating them to specific lemmas (and parts of lemmas) from pages 252-257 of Huth and Ryan.