This course will provide an introduction to mathematical logic from the perspective of computer science, emphasizing logic as a foundation of computer science, with strong connections to reasoning with programs, computability theory, complexity theory, and symbolic intelligence. The topics covered will be motivated by applications in artificial intelligence, databases, formal methods, formal verification, and theoretical computer science. The goal of the course is to prepare students to use logic as a formal tool in computer science. The course will also touch upon emerging techniques for machine learning symbolic logic from data. The course will roughly cover the following topics: propositional logic, SAT-solvers, first-order logic, completeness of FOL using quantifier instantiations, incompleteness theorems, decidable fragments of various first-order theories and using SMT solvers that decide them effectively.
We will use no standard textbook that spans the entire course; most parts of the course is covered by a new textbook being written from the experience of teaching these course, by Madhusudan and Viswanathan. All other course material will be available online as well.
Prerequisites: Students should have taken CS173 (or a similar course) and be able to do basic proofs using induction and proofs by contradiction (as taught in CS173). Some background on computability theory (as taught in CS374) would be good. Students who have not taken any course on computability theory (CS374) should inform the instructor; they will be given extra material to catch up on these topics.
