CS 474 - Logic in Computer Science (Spring 2023)

Madhusudan Parthasarathy (aka Madhu)

Tue and Thu 9:30am-10:45am, 1304 Siebel Center

Instructor
Madhusudan Parthasarathy
Lectures
Lecture Schedule
Teaching Assistant
Adithya Murali
Office Hours (on zoom) every Friday from 10 AM to 11 AM zoom link
Resources
Papers, textbook chapters, tools
Homework
We will use gradescope for submitting assignments
Homework Schedule will be posted soon
Piazza
http://piazza.com/illinois/spring2023/cs474
Access code sent to registered students on their illinois email

 

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

Initial Logistics
WARNING: these pages are still tentative. Don't trust the details until the first few lectures are done.