CSci 420/520: Homework 5

Modeling in PVS

Due Friday, Oct 14th by 1pm.

Summary

This assignment will introduce the basics for writing specifications in PVS, and expose you to more substantial proofs. You are given a logic puzzle. The goal is to translate the puzzle into a PVS model and then use the model to solve the puzzle.

The Puzzle

In this assignment we focus on writing models in PVS. The following is a description of the logic puzzle in English. You are to translate this puzzle into PVS and then solve it.

A young woman attending a party was introduced to four men in rather rapid succession and, as usual at such gatherings, their respective types of work were mentioned rather early in the conversation. Unfortunately, she was afflicted with a somewhat faulty memory. Half an hour later, she could remember only that she had met a Mr. Brown, a Mr. White, a Mr. Black, and a Mr. Green. She recalled that among them were a photographer, a grocer, a banker and a singer, but she could not recall which was which. Her hostess, a fun-loving friend, refused to refresh her memory, but offered four clues. Happlily, the young woman's logic was better than her memory, and she quickly paired each man with his profession. Here are the clues:

1. Mr. White approached the banker for a loan.
2. Mr. Brown had met the photographer when he hired him to take pictures of his wedding
3. The singer and Mr. White are friends but they have never had business dealings.
4. Neither Mr. Black nor the singer had ever met Mr. Green before that evening.

Instructions

Download logic.pvs and save it in your work directory.

Follow the instructions in the file to write the necessary functions. The puzzle statement will help you translate the problem into PVS.

Verify your program is valid by checking the syntax using M-x tc. You should not have any errors or TCCs generated.

Solve the problem by finding a counterexample to the conjecture at the end of the proof file. In effect, you will be trying to find a counterexample to the claim "There is no solution to the problem".

You should be able to find the counterexample using the commands: (prop), (lemma), (grind), (case), (hide), (reveal), (inst), (skolem!), (assert), and (split). However, feel free to use whatever commands you want.

Hints

If your model is incorrect, you will have a hard time with the conjecture. If you want me to grade your model before you start working on the proof, just email it to me. (Please do this well in advance of the due date.)

When you are done working on the conjecture, your PVS proof window should look like this:

puzzle.1.1.1 :  

[-1]  job!1(green) = something
[-2]  job!1(white) = something
[-3]  job!1(black) = something
[-4]  job!1(brown) = something
  |-------

Rule? (quit)

Note that the proof tree has three side branches ("puzzle.1.1.1"), each branch corresponding to the use of the (case) operation for one of the jobs above. Be careful of commands such as (prop) that will automatically create extra cases--you want to only create new cases using (case).

Keep in mind that statements in the succeedent can be interpreted as negated in the antecedent. In effect you will be building up a list of jobs that a person cannot have in the succeedent. For example:

[-1]  some formulas
|-------
[1]   job!1(white) = banker
[2]   job!1(brown) = photographer
[3]   job!1(white) = singer
[4]   job!1(black) = singer
[5]   job!1(green) = singer

The above says that none of Messrs White, Black, or Green can be the singer. At this point we have enough information to conclude that Mr. Brown must be the singer, so we can issue a (case "job!1(brown)=singer"). This will yield two branches, the first of which is the one that leads to a solution. The second one needs to be proven to not be the solution, however, so you would need to (postpone), then use the "all_job_allocated" lemma and (prop) to show that this branch is true (and therefore not the solution).

Your strategy should not be to immediately issue a (case "job!1(brown)=some guess") statement and then try to prove the second branch. This will take a long time and will lead to a lot of frustration. Rather, first manipulate the sequents until you reach one that is pretty obviously true, like the one above. Then issue your case statement and do the easy proof of the second branch.

Use (hide) to remove unnecessary formulas. Use (typepred "job!1") to get the facts that the job mapping is one-to-one and onto. Try using the "onto" property, and the lemmas provided.

At one point you will need to use the last quantification to instantiate two people. Try "brown" and "green".

Grading

250 points total

A valid solution will be a proof tree with three splits. Three side-branches of the proof will be proven, while the remaining branch will be unproven, and will contain the counterexample that is the answer shown above.

For bonus points, prove the lemmas as well. You may need to read up on lemmas that PVS automatically creates for enumerated types.

Email your logic.pvs and logic.prf files to meghan@cs.wm.edu.