The first homework consists of two parts. The first is a very simple sets of problems for PVS. Prove the following claims.

The second part of the homework is to attempt to formalize one of the problems on the Common sense problems page. Write no more than twenty formulas.

Finally, PVS is running on Steam again. It is in /u/costello/pvs/source/pvs. The first part of the homework is to prove that the missionaries and cannibals problem is solvable. Prove the claims in tuple.pvs and tuple5.pvs. The first says that the Missionaries and Cannibals problem is solvable when there are three missionaries and cannibals, the second says it is not solvable when there are four.

The second part of the homework also involves PVS. It is easier. It involves showing that minimizing the disjunction of two minimized terms makes no difference. Prove the two claims in filter.pvs.

The final part of the homework is more open ended. Prove as many of the statements about blocksworld in blocks.pvs. These problems are quite hard.

T Costello
Last modified: Thu Apr 16 12:25:38 PDT 1998