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?

• (Optional but highly recommended) Solve this problem yourself with paper and pencil.

• Compare your method of solution with the one described in the logic-puzzle book [PDF]

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.

• Prove all the the lemmas, verifying that the solution is correct. Use only (SPLIT), (FLATTEN), (PROP), (INST), (SKOLEM), (LEMMA), (SIMPLIFY), and (ASSERT).

• P415 Students: You are provided with a C.prf file containing the proof of Lemma L6. You can review this proof with the PVS command M-x xsp, to raise a buffer containing the proof. In that buffer, the key sequence TAB-1 executes the next step of the proof.

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

• (Optional but highly recommended) Write out pencil-and-paper proofs of Propositions D_2 and D_6.

• Prove Propositions D_1 through D_9. In addition to the commands above, you will need (EXPAND) and (REPLACE).

• P515 Students: Theorem D_10 cannot be proven using the commands listed above. It is true, of course, so how would you prove it? Be ready to present your argument in class.