Assignment 1

Meet PVS

Instructions:

1. Copy the PVS source files A.pvs, B.pvs, and C.pvs to an appropriate place on your computer (which should already have PVS installed on it).
2. Move to the directory containing the files and invoke pvs5. Using PVS, prove all the theorems in each file. Further instructions, restricting what proof-commands to use, are included as comments in these source files.
3. When you are done proving the theorems, while still in PVS, enter the command M-x prove-pvs-file to generate a buffer containing a status report. Save this buffer (using C-x C-w) under the name A.status (B.status, C.status respectively).
4. PVS has now created new files, A.prf, and B.prf and C.prf recording the proofs you have done; and A.status, B.status and C.status recording the status of your work. The files C.* should be handed in via Blackboard, using the corresponding assignment.

   Notes and Hints:

   • During the lectures, the following PVS system commands were used:

     • M-x ff opens a PVS source file (.pvs)

     • M-x pr initiates a proof of the theorem under the cursor (i.e. open the PVS proof editor).

   • The instructions in A.pvs, B.pvs, and C.pvs say what prover commands to use to complete the proofs:
     • For A.prf may use only the commands (SPLIT f) and (FLATTEN f). Your learning goal is to know (not guess) which command to use at a given point in the proof.
     • For B.prf you may use only the commands (SPLIT f), (FLATTEN f), (SKOLEM f name), and (INST f expression), Again, you want to get to the point of knowing (not guessing) which command to use and when.
     • For C.prf, in addition to (SPLIT), (FLATTEN), (SKOLEM) and (INST), You may use the commands Use only (PROP), (LEMMA), (SIMPLIFY), and (ASSERT).

   • The prover's quantifier elimination commands are (It is important to include the quotation marks):

     • (INST f "t") instantiates the for-all (in the antecedent) or there-exists (in the conclusion) variable in formula i with the term t. For example,

       {-1} (FORALL x: P(x)) |------- {1} ... Rule? (inst -1 "f(a)") {-1} P(f(a)) |------- {1} ... Rule?

     • (SKOLEM f "v") introduces the skolem constant (dummy name) for the there-exists (in the antecedent) or for-all (in the consequent) variable in formula i. Example:

       {-1} (EXISTS x: NOT P(x)) |------- {1} ... Rule? (skolem -1 "A") {-1} NOT P(A) |------- {1} ... Rule?

   • (SIMPLIFY) and (ASSERT) invoke PVS's arithmetic reasoning procedures. They are used when the goal formula(s) involve: Assertions about equality or inequality.
   • (LEMMA "name") introduces a previously established fact (axiom, theorem, etc.) to the sequent.

   • 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?

     • Solve this problem yourself with paper and pencil.