Classes start in the week of August 30, 2021.
This schedule may change throughout the semester. Check back regularly for updates, including assignment deadlines and other important dates.
date | topic | notes |
8/31/21 | Introduction | intro.pdf |
9/2/21 | Induction and Recursion | Assignment 1 due |
9/7/21 | Structural Induction and Invariants | invariants.pdf |
9/9/21 | Using Lean I | Assignment 2 due |
9/14/21 | Using Lean II | |
9/16/21 | Propositional Logic I | prop.pdf, Assignment 3 due |
9/21/21 | Propositional Logic II | normalforms.pdf |
9/23/21 | Implementing Propositional Logic I | Assignment 4 due |
9/28/21 | Exam I | |
9/30/21 | Implementing Propositional Logic II | |
10/5/21 | SAT Solving Basics | sat-basics.pdf |
10/7/21 | Using SAT Solvers | using-sat.pdf, Assignment 5 due |
10/12/21 | Conflict-Driven Clause Learning | cdcl.pdf |
10/14/21 | Mid-semester break (no classes) | |
10/19/21 | Deduction and Search | |
10/21/21 | Terms and Formulas I | Assignment 7 due |
10/26/21 | Terms and Formulas II | |
10/28/21 | First Order Logic | Assignment 8 due |
11/2/21 | Exam II | |
11/4/21 | Implementing First Order Logic I | Assignment 9 due |
11/9/21 | Implementing First Order Logic II | |
11/11/21 | Decision Procedures for First Order Logic | |
11/16/21 | SMT solvers | smt.pdf |
11/18/21 | Using SMT solvers | using-smt.pdf |
11/23/21 | Deduction for First Order Logic | |
11/25/21 | Thanksgiving (no classes) | |
11/30/21 | First Order Logic in Lean | |
12/2/21 | Simple Type Theory | |
TBD | Final Exam |