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