This schedule may change throughout the semester.
Check back regularly for updates, including assignment deadlines and other important dates.
The assignments are availble on Gradescope
The postfix (F22) indicates that the material is of Fall'22.
| date | topic | notes |
| 01/17/2024 | Introduction, Induction, and Invariants | introduction-S24.pdf |
| 01/22/2024 | Introduction using Lean | lean |
| 01/24/2024 | Propositional Logic | lean prop.pdf, Assignment 1 due |
| 01/29/2024 | Normal Forms | normalforms.pdf |
| 01/31/2024 | Implementing Propositional Logic | lean, Assignment 2 due |
| 02/05/2024 | Basic SAT techniques | basic-SAT-techniques.pdf, lean |
| 02/07/2024 | Basic SAT Solving | basic-SAT-solving.pdf, lean, Assignment 3 due |
| 02/12/2024 | DP and DPLL | DP-DPLL.pdf |
| 02/14/2024 | Conflict-Driven Clause Learning | CDCL.pdf, Assignment 4 due |
| 02/19/2024 | Exam I | practice1.pdf, practice1_solutions.lean, practice1_solutions.pdf |
| 02/21/2024 | Deduction for Propositional Logic | |
| 02/26/2024 | Lean as a Proof Assistant I | lean |
| 02/28/2024 | First-order logic | FOL.pdf, Assignment 5 due |
| 03/04/2024 03/06/2024 |
Spring break (no classes) | |
| 03/11/2024 | Lean as a Proof Assistant II | lean |
| 03/13/2024 | Implementing First-Order Logic | lean, Assignment 6 due |
| 03/18/2024 | Unification | unification.pdf |
| 03/20/2024 | Congruence Closure | congruence-closure.pdf, Assignment 7 due |
| 03/25/2024 | Exam II | practice2.pdf, practice2_solutions.pdf |
| 03/27/2024 | Decision Procedures and Linear Arithmetic | |
| 04/01/2024 | SMT Basics | smt.pdf |
| 04/03/2024 | Using SMT Solvers | using-smt.pdf, Assignment 8 due |
| 04/08/2024 | Deduction for First Order Logic | |
| 04/10/2024 | Automated Theorem Proving for First-Order Logic | resolution.pdf, Assignment 9 due |
| 04/15/2024 | Using First-Order Theorem Provers | |
| 04/17/2024 | Lean as a Proof Assistant III | lean |
| 04/22/2024 | Computer-Generated Propositional Proofs | prop-proofs.pdf |
| 04/24/2024 | Higher-order Logic and Beyond | lean, Assignment 10 due |
| 05/02/2024 | Final Exam | practice3.pdf, practice3_solutions.pdf |