CSCI P415/515 Fri Jan 6 15:18:04 EST 2012 [SDJ]

Homework Assignment

In your SVN subdirectory 2/ you will find two PVS source files. You are to prove some or all of the theorems in these files, as instructed below. Deposit all resulting *.status, *.prf, and *.pvs files to your SVN directory.

  1. C.pvs is a PVS theory containing a formulation of the problem below and its solution:
    Andy, Bob, Cindy, Dinah, Eve, Fred, and Gary live in the seven houses, numbered 1 through 7, on Maple Steet. Gary's address is 5 greater than Bob's. Bob's address is greater than Andy's. Dinah's address is less than Eve's, whose address is 2 less than Gary's. Cindy's address is less than either Dinah's or Fred's. Who lives where?

    In the PVS formulation, the problem statement, together with some needed background knowledge, are expressed as axioms (assumptions). The solution is represented by a series of lemmas.

  2. D.pvs defines even and odd natural numbers, and states several properties about them.