This schedule may change throughout the semester.
Check back regularly for updates, including assignment deadlines and other important dates.
The postfix (F21) indicates that the material is of last year.
| date | topic | notes |
| 08/29/2022 | Introduction | intro.pdf |
| 08/31/2022 | Induction and Recursion | Assignment 1 due |
| 09/07/2022 | Structural Induction and Invariants, Using Lean I | invariants.pdf, lean, Assignment 2 due |
| 09/12/2022 | Using Lean II | lean |
| 09/14/2022 | Propositional Logic I | prop.pdf, Assignment 3 due |
| 09/19/2022 | Propositional Logic II | normalforms.pdf |
| 09/21/2022 | Implementing Propositional Logic I | lean, Assignment 4 due |
| 09/26/2022 | SAT Solving Basics | sat-basics.pdf |
| 09/28/2022 | Implementing Propositional Logic II | lean, Assignment 5 due |
| 10/03/2022 | Exam I | practice1.pdf, practice1.lean, practice1_solutions.pdf |
| 10/05/2022 | Using SAT Solvers | using-sat.pdf |
| 10/10/2022 | Deduction for Propositional Logic I | |
| 10/12/2022 | Deduction for Propositional Logic II | lean, Assignment 6 due |
| 10/17/2022 10/19/2022 |
Mid-semester break (no classes) | |
| 10/24/2022 | Propositional Logic in Lean | lean |
| 10/26/2022 | Conflict-Driven Clause Learning | cdcl.pdf, Assignment 7 due |
| 10/31/2022 | First-order Logic | |
| 11/02/2022 | Implementing First Order Logic I | lean, Assignment 8 due |
| 11/07/2022 | Exam II | practice2.pdf, practice2_solutions.pdf |
| 11/09/2022 | Implementing First Order Logic II | lean |
| 11/14/2022 | Decision Procedures for First Order Logic I | |
| 11/16/2022 | SMT solvers | smt.pdf (F21), Assignment 9 due |
| 11/21/2022 | Deduction for First Order Logic II | |
| 11/23/2022 | Thanksgiving (no classes) | |
| 11/28/2022 | Using SMT solvers | using-smt.pdf |
| 11/30/2022 | Using First-Order Theorem Provers | Assignment 10 due, lean |
| 12/05/2022 | Deduction for First-order Logic | |
| 12/07/2022 | First-Order Logic in Lean | Assignment 11 due |
| 12/13/2022 | Final Exam at 5:30pm in GHC 5222 | practice3.pdf, practice3_solutions.pdf |