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