§P415 Homework Assignment

Instructions:

1. Copy the PVS source files, I.pvs and J.pvs.

2. Using PVS, prove the theorems in each file. Note that in J.pvs you will need to add one or more theorems to the file.

Notes and Hints:

• The PVS source files contain additional instructions and hints.

• These problem sets are a bit deeper mathematically than the earlier assignments. It is highly advisable to work out the proofs by hand before attempting them in PVS.

• If the proofs are done "right" (i.e., in a way that best sets up the PVS decision procedures), assert is enough to finish them off. However, it is easy to make mistakes, such as expanding function definitions too far. You can sometimes avoid this by doing more manually guided case-splitting, using lift-if and case. As always, this technique will be demonstrated in lecture.