Homeworks
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