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 |