§P415 Homework Assignment

Instructions:

2. Copy the PVS source files C.pvs and D.pvs into your local subdirectory 2/

3. Using PVS, prove the theorems in each file
   

   Note: THEOREM D_12 is optional; it is just something to play around with to see what PVS might know about numbers.

Notes and Hints:

• The PVS source files contain additional instructions. In C.pvs proofs you are to use only SPLIT, FLATTEN, INST, SKOLEM, LEMMA and ASSERT.

• In D.pvs proofs you may need EXPAND, REPLACE and SIMPLIFY in addition to the commands above.

• I recommend that you first solve the problem in C.pvs without referring to the axioms and lemmas in the file. Then read through the file to see how the solution is formulated in PVS. After that, prove the theorems. You may prove them in any order you wish, but doing the proofs in order is recommended.

• I strongly recommend that before attempting the proofs in D.pvs, you first write out pencil-and-paper proofs.