Logic for Computer Science
Time and place: Tuesday and Thursday 5:00-6:20pm, CSE 2154
Office hours: Wednesday 4-5pm, Thursday 6:30 - 7:30pm, CSE 4238
TA: Yuliang Li
TA office hour: Tuesday 11am-12pm, CSE 3240
The goal of this course it to introduce students to
mathematical logic as a tool in computer science.
After covering basic material on propositional and predicate logic, the course
presents the foundations of finite model theory
and descriptive complexity. Other topics, including
temporal logic, model checking,
and reasoning about knowledge and belief, will be discussed as time allows.
Evaluation is based on homework sets and a take-home final.
Notes and books: class notes taken by volunteer scribes will be made available along the way.
There is no single text for the class, but useful references include the following:
- C. H. Papadimitriou: Computational Complexity, Addison Wesley 1994 (Part II: Logic)
- L. Libkin: Elements of Finite Model Theory, Springer 2004
- S. Abiteboul, R. Hull, V. Vianu: Foundations of Databases, Addison Welsey 1995
- N. Immermann: Descriptive Complexity, Springer 1999
(Thanks to past and present scribes!)
- Propositional Logic (pdf) (latex)
- First-Order Logic and Gödel's Completeness Theorem (pdf)
Please typeset your solutions (latex recommended)
Readings and Links
- Moshe Vardi's talk "From Aristotle to the Pentium" (slides)
- Phokion Kolaitis and Moshe Vardi: Logic as the calculus of computer science (pdf)
- Moshe Vardi's brief history of logic (pdf)
- Christos H. Papadimitriou on logic and computing: slides and voice, speaker(Windows Media WMV files)
- Reasoning about Knowledge: survey by J. Halpern ( pdf)
- A novel of Love and Logic: Turing (pdf) by Christos H. Papadimitrou (Rated R). Find the technically lighter published version here
- Review: undecidability of the Halting Problem (Dr. Seuss style)