CS222 - Winter Quarter

Gates B12, 12.50-2.05 MW

The Final is now available. It is due Wednesday Night.

The Midterm is now available. It is due Wednesday Night.

A course outline gives the topics for each lecture, and some readings.


The next reading is chapter 9 of the textbook and Allen's theory of time.

The first two weeks readings were::
   A Framework for Representing Knowledge Especially the criticism of the Logistic approach.

   Programs with Common Sense This is the classic paper suggesting the use of logic for representing information in computers.

  The introduction of the textbook (chapter 1), Knowledge Representation and Reasoning is also relevant.

The unexpected hanging is covered in Montague and Kaplan's classic paper. Montague's "Syntactic Treatments of Modality, with Corollaries on Reflection Principles and Finite Axiomatizability." is not online.

For modal logic this page is the best overview I have found. You can ignore relevance logic and provability logics.

The Snark theorem prover's home page is useful, as is their manual.

Mailing List

A mailing list cs222 has been setup. Please add yourself to the mailing list, or send me email and I can add you.


The first homework will be due on January 24th. It will be some C programming. The homework will be given out on Monday, 10th.

The second homework will be due on February 7th. It will be some axiomatization in SNARK.

Notes for the lecture on Monday the 10th are available here.
Notes for the lecture on Wednesday the 12th are available here (Completeness) and here(Resolution).

Two theorem provers PVS and Snark will be used in the course. These are both written in Lisp, but no knowledge of Lisp is needed for the course.