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 (S24) indicates that the material is of Spring'24.
| date | topic | notes |
| 01/14/2025 | Introduction, Induction, and Invariants | introduction.pdf |
| 01/16/2025 | Introduction using Lean | lean |
| 01/21/2025 | Propositional Logic | prop.pdf |
| 01/23/2025 | Normal Forms | normalforms.pdf, Assignment 1 due |
| 01/28/2025 | Implementing Propositional Logic | lean |
| 01/30/2025 | Basic SAT techniques | basic-SAT-techniques.pdf, Assignment 2 due |
| 02/04/2025 | Basic SAT Solving | basic-SAT-solving.pdf |
| 02/06/2025 | DP and DPLL | DP-DPLL.pdf, Assignment 3 due |
| 02/11/2025 | Conflict-Driven Clause Learning | CDCL.pdf |
| 02/13/2025 | Proof Systems for Propositional Logic | proof-prop.pdf, Assignment 4 due |
| 02/18/2025 | Exam I | practice1.pdf, practice1_solutions.lean, practice1_solutions.pdf |
| 02/20/2025 | Lean as a Proof Assistant I | lean |
| 02/25/2025 | First-order logic | FOL.pdf |
| 02/27/2025 | Lean as a Proof Assistant II | lean, Assignment 5 due |
| 03/04/2025 03/06/2025 |
Spring break (no classes) | |
| 03/11/2025 | Implementing First-Order Logic | lean |
| 03/13/2025 | Unification | unification.pdf, Assignment 6 due |
| 03/18/2025 | Congruence Closure | congruence-closure.pdf |
| 03/20/2025 | Decision Procedures and Linear Arithmetic | linear-arithmetic.pdf, Assignment 7 due |
| 03/25/2025 | Exam II | practice2.pdf, practice2_solutions.pdf |
| 03/27/2025 | SMT Basics | smt.pdf |
| 04/01/2025 | Using SMT Solvers | using-smt.pdf (S24) |
| 04/03/2025 | Spring carnival (no class) | |
| 04/08/2025 | Deduction for First Order Logic | |
| 04/10/2025 | Automated Theorem Proving for First-Order Logic | resolution.pdf (S24), Assignment 8 due |
| 04/15/2025 | Using First-Order Theorem Provers | |
| 04/17/2025 | Lean as a Proof Assistant III | lean (S24), Assignment 9 due |
| 04/22/2025 | Computer-Generated Propositional Proofs | prop-proofs.pdf (S24) |
| 04/24/2025 | Higher-order Logic and Beyond | lean (S24), Assignment 10 due |
| 05/01/2025 | Final exam (scheduled at 8:30am, but we start at 10:00am) | practice3.pdf, practice3_solutions.pdf |