CS 323: Applications of Nonmonotonic Reasoning - Homework Assignments

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.

Homework #4 (ps format) is due on Mar. 13th.

Good Luck