- Draft of Lecture Notes by P. Madhusudan and Mahesh Viswanathan.
- Mediaspace channel with lecture recordings.

- Instructor: Mahesh Viswanathan
- Lectures:

Tu/Th 9:30am to 10:45am on zoom - Office Hours:

Tu/Th 10:45am to 11:30am on zoom - Discussion Group: Campuswire

Discussion board link and access code can be found here

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.

__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.

- Lecture 01 [Aug 24]: Propositional logic syntax and semantics. Sections 1.1 through 1.3 (except Cook-Levin Theorem).
**[video, scribbles]** - Lecture 02 [Aug 26]: Compactness Theorem. Section 1.4.
**[video, scribbles]** - Lecture 03 [Aug 31]: Proof Systems. Sections 2.1 and 2.2 (until 2.2.2).
**[video, scribbles]** - Lecture 04 [Sep 02]: Completeness of Resolution and recap of recursive enumerability and decidability. Sections 2.2.2, and A.1 to A.3. For details on Church-Turing thesis see supplementary notes.
**[video, scribbles]** - [Sep 02]: Homework 1 due 9/9.
- Lecture 05 [Sep 07]: Recap of Computability. Sections A.3, A.4. For more examples on reductions see supplementary notes.
**[video, scribbles]** - Lecture 06 [Sep 09]: Introduction to Complexity Theory. Sections A.5, A.6.
**[video, scribbles]** - Lecture 07 [Sep 14]: P, NP, and coNP. Sections A.7, 1.3 (Cook-Levin Theorem).
**[video, scribbles]** - Lecture 08 [Sep 16]: Craig's Interpolation Theorem and Proof Complexity. Section 2.3.
**[video, scribbles]** - [Sep 16]: Homework 2 due 9/23.
- Lecture 09 [Sep 21]: Proof Complexity. Section 2.3.
**[video, scribbles]** - Lecture 10 [Sep 23]: First order logic. Chapter 3.
**[video, scribbles]** - Lecture 11 [Sep 28]: Quantifier Elimination: Dense Linear Orders without Endpoints. Chapter 4 until the end of section 4.1.
**[video, scribbles]** - Lecture 12 [Sep 30]: Quantifier Elimination: Linear Arithmetic. Section 4.2.
**[video, scribbles]** - Lecture 13 [Oct 05]: Church-Turing Theorem: Undecidability of Validity. Chapter 5 upto section 5.3.
**[video, scribbles]** - Lecture 14 [Oct 07]: Validity of Universally quantified sentences.
**[video, scribbles, Madhu's notes]** - [Oct 07]: Homework 3 due 10/15.
- Lecture 15 [Oct 12]: Completeness Theorem Part I.
**[video, scribbles, Madhu's notes]** - Lecture 16 [Oct 14]: Completeness Theorem Part II.
**[video, scribbles, Madhu's notes]** - Lecture 17 [Oct 19]: Godel's Incompleteness Theorem.
**[video, scribbles, Madhu's Notes]** - Lecture 18 [Oct 21]: Finite Model Theory. Trakhtenbrot's Theorem Section 5.3.
**[video, scribbles, old notes]** - Lecture 19 [Oct 26]: Ehrenfeucht-Fraisse Games and the Expressive power of First Order Logic part I.
**[video, scribbles, old notes]** - Lecture 20 [Oct 28]: EF Games part II.
**[video, scribbles, old notes]** - [Oct 28]: Homework 4 due 11/05.
- Lecture 21 [Nov 02]: Descriptive Complexity.
**[video, scribbles, second order logic, Sections 3.1.5, 3.2.1]** - Lecture 22 [Nov 04]: Descriptive Complexity: Consequences of Fagin's Theorem and Immerman-Vardi Theorem.
**[video, scribbles, Sections 3.1.5, 3.2.1]** - Lecture 23 [Nov 09]: Tree Automata.
**[video, scribbles, old notes]** - Lecture 24 [Nov 11]: Monadic Second Order Logic on trees.
**[video, scribbles, old notes]** - Lecture 25 [Nov 16]: Tree Decomposition and Tree width.
**[video, scribbles, old notes]** - Lecture 26 [Nov 18]: Courcelle's Theorem.
**[video, scribbles, old notes]** **[Nov 20] to [Nov 28]:**Fall Break!- Lecture 27 [Nov 30]: Courcelle's Theorem (proof completed)
**[video, scribbles, old notes]** - Lecture 28 [Dec 02]: Intuitionistic Propositional Logic.
**[video, scribbles, Sections 2.1, 2.5, 2.6, 5.3]** - Lecture 29 [Dec 07]: Combinatory Logic and Curry-Howard Isomorphism.
**[video, scribbles, Sections 5.1, 5.2, 5.3]** **Final Exam**Monday December 13, 8am to 11am. Zoom link.