Course contents
- In this course, we will study the foundations of symbolic logic for computer science and computer scientists. We will deal with various aspects of logical reasoning about systems and programs as well as cover some applications.
Logic as a calculus for formal reasoning
Satisfiability - the problem and the solution
How to reason logically about programs?
Temporal Logics and Model Checking
Broadly we plan to cover the following topics in this course:
Textbook References
- Logic in Computer Science. Michael Huth and Mark Ryan, Cambridge Press, Second Edition. Indian Edition available.
- Principles of Model Checking. Christel Baier, Joost P.Katoen, MIT Press, Official online copy available. More lecture notes, tutorial links will be provided later.
Topics covered
| Date | Topics covered | Resources | Reference |
|---|---|---|---|
| Jul 28, Lecture 0 | Introduction, course outline | Slides | |
| Jul 30, Lecture 1 | Module 1: Propositional Logic - Logic Puzzles and Syntax | Slides | Huth & Ryan, Sections 1.1, 1.3 |
| Aug 04, Lecture 2 | Module 1: Propositional Logic - Parse Trees, Semantics and Problems of Interest | Slides | Huth & Ryan, Sections 1.3, 1.4, 1.5.1 |
| Aug 06, Lecture 3 | Module 1: Propositional Logic - Formal Proofs and Natural Deduction | Slides | Huth & Ryan, Section 1.2 |
| Aug 11, Lecture 4 | Module 1: Propositional Logic - Natural Deduction Rules | Slides | Huth & Ryan, Sections 1.2, 1.2.1 |
| Aug 13, Lecture 5 | Module 1: Propositional Logic - Soundness and Completeness of Natural Deduction | Slides | Huth & Ryan, Sections 1.2.1, 1.2.5, 1.4.3, 1.4.4 |
| Aug 18, Lecture 6 | Module 1: Propositional Logic - Completeness of Natural Deduction | Slides | Huth & Ryan, Section 1.4.4 |
| Aug 20, Lecture 7 | Module 1: Propositional Logic - Normal Forms (NNF, CNF, DNF) and Tseitin's Encoding | Slides | Huth & Ryan, Sections 1.5, 1.5.2, ++ |
| Aug 25, Lecture 8 | Module 2: The Problem of Satisfiability - (Propositional) Resolution | Slides | Stanford, Introduction to Logic, Chapter 6: Resolution Proofs |
| Aug 27, Lecture 9 | Module 2: The Problem of Satisfiability - The DPLL Algorithm | Slides | Ruben Martins, CMU 15-414, Lecture 16: Solving SAT with DPLL |
| Aug 28 | Quiz 1 | ||
| Sep 01, Lecture 10 | Module 2: The Problem of Satisfiability - Clause Learning and the CDCL Algorithm | Slides | Marques-Silva, Lynce, Malik, Handbook of Satisfiability, Chapter 4: Conflict-Driven Clause Learning SAT Solvers |
| Sep 03, Lecture 11 | Module 2: The Problem of Satisfiability - A Tool Demo: Solving Puzzles with a SAT-Solver (Z3) | Slides | Microsoft, Online Z3 Guide, Programming Z3 (Python) - Introduction |
| Sep 08, Lecture 12 | Module 3: Predicate Logic - Syntax of Predicate Logic | Slides | Huth & Ryan, Sections 2.2, 2.2.1, 2.2.2, 2.2.3 |
| Sep 10, Lecture 13 | Module 3: Predicate Logic - Semantics of Predicate Logic | Slides | Huth & Ryan, Sections 2.4, 2.4.1, 2.4.2, 2.4.3, 2.5 |
Notes:
- Being a core CSE department course, CS228 will not be open for non-CSE students this semester. Interested non-CSE students are advised to consider one of the relevant minor courses being offered by the CSE dept this semester.