Class Text

Supplemental Texts

Lecture Notes

Lecture notes for the first several classes are at pdf/outline.pdf. The source is in the directory lectures.

Code fragments are in the directory Code.

Class Mailing list:

The web page for users of your mailing list is:

There is also an email-based interface for users (not administrators)
of your list; you can get info about using it by sending a message
with just the word `help' as subject or in the body, to:

Other Courses


Huth and Ryan introduce logic with a focus on algorithms. It will be the primary resource for the class. It covers propositional logic, predicate logic, and the modal logics foundational to model checking. It also discusses SAT solving and related techniques in some detail.

Fitting and Nerode and Shore both use Smullyan's technique of tableau proof for elementary provers for propositional and predicate logic. The proof theory and the model theory are very closely related with this technique, making proofs of completeness straightforward.

Topical links:

Links that come up in lecture notes and such. Added more or less in chronological order: