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, Assignment 3 due |
| 02/10/2026 | Conflict-Driven Clause Learning | CDCL.pdf |
| 02/12/2026 | Proof Systems for Propositional Logic | proof-prop.pdf, Assignment 4 due |
| 02/17/2026 | Exam I at 6pm in Porter Hall 100, no class | practice1.pdf, practice1_solutions.lean, practice1_solutions.pdf |
| 02/19/2026 | Lean as a Proof Assistant I | lean |
| 02/24/2026 | Lean as a Proof Assistant II | lean |
| 02/26/2026 | First-order logic | FOL.pdf, 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 at 6pm in Porter Hall 100, no class | 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 |
| April 30, 5:30-8:30pm (tentative) | Final exam | practice3.pdf, practice3_solutions.pdf |