Homework #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.
Homework #1 due on Tuesday Jan. 21st
Homework #2 (ps format) was due on Feb. 4th, and was already returned. The solutions (ps format) are available, as well as the pvs files for the MCP problem (thanks to Martina Faller).
Homework #3 (ps format) was due on Feb 18th, and was already returned. Solutions are coming soon.
Good Luck
