#
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

eyal@www-formal.stanford.edu