BE AWARE: This page is outdated. Visit the most recent version for up-to-date information.
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 |