- Spring 2017 offering of this class by Madhusudan Parthasarthy.
- A Mathematical Introduction to Logic, by H.B. Enderton.
- An Introduction to Logic by Madhavan Mukund and S.P. Suresh.
- Calculus of Computation by Aaron Bradley and Zohar Manna.
- Elements of Finite Model Theory by Leonid Libkin.

- Instructor: Mahesh Viswanathan
- TA: Lucas Pena
- Lectures:

Tu/Th 12:30pm to 1:45pm in 1103 Siebel - Office Hours:

Tu/Th 1:45pm to 3:00pm (Mahesh in 3232 SC)

W 2:00pm to 3:00pm (Lucas in 2111 SC) - Discussion Group: Piazza

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.

- Lecture 01 [Aug 28]: Propositional logic syntax and semantics.
**[notes]** - Lecture 02 [Aug 30]: Proof systems for propositional logic. Sections 1 and 2 of
**[notes]** - Lecture 03 [Sep 04]: Compactness Theorem. Section 3 of
**[notes]** - [Sep 06]:
**No lecture.**Mahesh is traveling. Homework 1 due 9/13:**[PDF, Tex]** - Lecture 04 [Sep 11]: Recap of recursive enumerability and decidability.
**[notes]**. For more details and examples consult supplementary notes on the Church-Turing thesis and reductions. - Lecture 05 [Sep 13]: Introduction to Complexity Theory. Sections 1 to 3 of
**[notes]** - Lecture 06 [Sep 18]: P, NP, and coNP. Sections 3 and 4 of
**[notes]** - Lecture 07 [Sep 20]: Craig's Interpolation Theorem and Proof Complexity.
**[notes]** - [Sep 21]: Homework 2 due on 10/2:
**[PDF, Tex]** - Lecture 08 [Sep 25]: First order logic. Sections 1 and 2 of
**[notes]** - Lecture 09 [Sep 27]: Godel's Completeness Theorem, Church-Turing Theorem. Sections 3 and 4 of
**[notes]** - Lecture 10 [Oct 02]: Godel's Incompleteness Theorem. Lecture 39 of Automata and Complexity by Kozen available through the library.
- Lecture 11 [Oct 04]: Linear Arithmetic and Quantifier Elimination. Sections 7.1 and 7.3 of Calculus of Computation.
- [Oct 08]: Homework 3 due on 10/16:
**[PDF, Tex]** - Lecture 12 [Oct 09]: Second Order Logic.
**[notes]** - Lecture 13 [Oct 11]: Buchi-Elgot-Trakhtenbrot Theorem. Sections 1 to end of 2.1 of
**[notes]** - Lecture 14 [Oct 16]: Presburger Arithmetic. Sections 2.2 onwards of
**[notes]** - Lecture 15 [Oct 18]: Automata on Infinite Words. Upto the end of Section 1.1 of
**[notes]** - Lecture 16 [Oct 23]: omega-regular languages. Sections 1.2 and 1.3 of
**[notes]** - Lecture 17 [Oct 25]: MSO on infinite words, S1S, and Complementation. Sections 1.4 and 1.5 of
**[notes]** - [Oct 29]: Homework 4 due on 11/9:
**[PDF, Tex]** - Lecture 18 [Oct 30]: Linear Temporal Logic. Upto the beginning of Section 2.1 of
**[notes]** - Lecture 19 [Nov 01]: Expressive power of LTL. Sections 2.1 and 3 of
**[notes]** - Lecture 20 [Nov 06]: Tree Automata. Sections 1 through 3 of
**[notes]** - Lecture 21 [Nov 08]: Monadic Second order logic on Trees. Sections 4 and 5 of
**[notes]** - Lecture 22 [Nov 13]: Finite Model Theory. Upto section 2 of
**[notes]** - Lecture 23 [Nov 15]: Ehrenfeucht-Fraisse Games and the Expressive power of First Order Logic. Section 2 of
**[notes]** **[Nov 17] to [Nov 25]:**Fall Break!- Lecture 28 [Nov 27]: Descriptive Complexity. Sections 3.1.5 and 3.2 of Finite Model Theory and Descriptive Complexity by Erich Graedel available through the library.
- Lecture 22 [Nov 29]: Series-Parallel Graphs and Monadic Second Order Logic.
**[notes]** - [Nov 30]: Homework 5 due on 12/7.
**[PDF, Tex]** - Lecture 23 [Dec 04]: Tree Decomposition and Tree width. Sections 1 to 3 of
**[notes]** - Lecture 24 [Dec 06]: Courcelle's Theorem. Section 4 of
**[notes]** - Lecture 25 [Dec 11]: Applications of Courcelle's Theorem. Section 5 of
**[notes]** **Final Exam**Monday December 17, 8am to 11am in 1109 Siebel.