CS 474: Logic in Computer Science

This course introduces mathematical logic from the perspective of computer science, emphasizing decidable fragments of logic and decision procedures.

Course Objectives. The goal of the course is to prepare students for using logic as a formal tool in computer science. By the end of course, students will be exposed to different fragments of logics and decision procedures for them, and connections between logic, algorithms and computational complexity. They will have seen tools and techniques that exploit logic to come up with algorithms to solve problems, and establish lower bounds. Students will be informed of some of the major open problems in the field and current efforts to solve them.

Course Contents. Motivated by applications in artificial intelligence, databases, formal methods and theoretical computer science, the course will roughly cover the following topics: Propositional Logic and Proof complexity, First order logic, decidable first order theories, monadic second order logic and regular languages, tree-width and Courcelle's theorem with applications to parametric complexity, finite model theory and descriptive complexity.

Prerequisites. This course is aimed for advanced undergraduate and graduate students interested in logic and theoretical computer science. Familiarity with basic logic and discrete mathematics (CS 173), basic algorithms and theory of computation (CS 374), and mathematical maturity will be expected.

Graded Work. There will one homework every 2 weeks (about 5 in total), and one final exam. The homework assignments and the final exam will be worth 50% each.

Collaboration. Limited collaboration is allowed for assignments, unless otherwise specified: you can discuss the problems with others in the class, and can submit solutions in groups of upto 3 students. In particular, you should not look at solutions written up by other groups. All collaboration should be declared.

Syllabus Statements. A link to syllabus statements is here.

Website Design. Thanks to Manoj Prabhakaran.

So far in the course

Lecture notes. Content will be regularly added to the draft by P. Madhusudan and Mahesh throughout the semester. The latest version can be found here. Chapters/sections/pages below refer to those in these notes.

Lecture videos. Mediaspace channel with video recordings is here.