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 for using logic as a formal tool in computer science. The course will also touch upon new techniques for machine learning symbolic logic from data, paving the path for unifying inductive and deductive reasoning. The course will roughly cover the following topics: propositional logic, SAT-solvers, first-order logic, proof systems, completeness and incompleteness theorems, decidable fragments of various first-order theories and SMT solvers to decide them effectively, descriptive complexity theory and finite model theory, program verification, and machine-learning of logic.
We will use no textbook that spans the entire course; some parts of the course will follow Enderton, which is available for students online. All other course material will be available online as well.
Prerequisites: Students should have taken CS173 (or a similar course) and know basic proofs using induction and proof by contradiction (as taught in CS173). Some background on computability theory (as taught is 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.
