CSE 205A
Logic for Computer Science
Instructor:
Victor Vianu
Email: vianu@cs.ucsd.edu
Phone: 858-534-6227
Time and place: Tuesday and Thursday 5:00-6:20pm, CSE 4217
First meeting: Tuesday, April 1st, CSE 3217
Office hours: Tuesday, Thursday 1-2pm, CSE 4238
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
logic programming, temporal logic, model checking,
and reasoning about knowledge and belief, will be discussed as time allows.
Evaluation is based on homework sets.
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
Scribe Notes
(Thanks to past and present scribes!)
- Propositional Logic (pdf)
Last updated 4/15
- First-Order Logic and Godel's Completeness Theorem (pdf)
Updated 4/29
- Godel's Incompleteness Theorem (pdf)
- Intro to Finite Model Theory (pdf)
Undecidability of finite satisfiability of FO (pdf)
- An application of FO: relational query languages (pdf).
- Ehrenfeucht-Fraisse games (pdf)
- 0-1 laws (pdf)
- Fixpoint and partial fixpoint: Chapter 14 in the Foundations book (starts on p.342) (pdf).
Note: the notation is slightly different from that used in class: FO on relations is denoted by CALC (for relational calculus).
Also, While is the same as partial fixpoint.
- Fixpoint vs. PTIME: Chapter 17 of the Foundations book (pdf). See Section 17.4
- Second-Order Logic (pdf).
To be updated soon.
- Introduction to temporal logic and model checking (pdf)
Assignments
Policy on collaboration.
Please typeset your solutions (latex recommended)
Readings and Links