This course provides an introduction to 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 and automata theory and between computational complexity and descriptive 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: syntax, semantics and proof theory of propositional logic, sat-solvers, syntax of first-order, the resolution proof system, syntax of second-order logic, connections between monadic second order logic and regular languages (word and tree, finite and infinite), tree-width and Courcelle's theorem with applications to parametric complexity, finite model theory and descriptive complexity, games and inexpressiveness.
Prerequisites. This course is aimed at 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.
Website Design. Thanks to Manoj Prabhakaran.