Problem Set #1 (ps format) includes a problem requiring the use of a theorem prover called PVS. In order to accomplish your task regarding the PVS, I hereby provide three documents that will hopefully serve you well. These are, the source of my Elementary1-MCP (the Elementary-MCP with 1 Missionary and 1 Cannibal) the problem solvability proof (as put into the PVS), and the same proof as LaTeX-ed by the PVS.
Problem Set #2 (ps format) due on 2/28/96.
The last Problem Set #3 (ps format) is due on 3/22/96. It requires you to copy and use the Set Theoretic Formalization of the MCP.
Good Luck
