Schedule
Sometimes, there is supplemental lecture material, but you are expected to attend and take notes.| Date | Lecture Notes | Extra | Due | |
|---|---|---|---|---|
| Tue | 01/14 | Overview | ||
| Wed | 01/15 | Rec: Propositions, judgements, proofs | ||
| Thu | 01/16 | Natural Deduction | ||
| Tue | 01/21 | Proofs as Programs | HW 1 | |
| Wed | 01/22 | Rec: Proof term tutch | code | |
| Thu | 01/23 | Harmony | ||
| Tue | 01/28 | Verifications | HW 2 | |
| Wed | 01/29 | Rec: Harmonic tutch and verifications | ||
| Thu | 01/30 | Quantification | ||
| Tue | 02/04 | Heyting Arithmetic | HW 3 | |
| Wed | 02/05 | Rec: Recurse in tutch | ||
| Thu | 02/06 | Induction/Recursion | code | |
| Tue | 02/11 | Review | HW 4 | |
| Wed | 02/12 | Rec: Practice | ||
| Thu | 02/13 | Midterm I | ||
| Tue | 02/18 | Sequent Calculus | ||
| Wed | 02/19 | Rec: Natural deductions versus sequents | ||
| Thu | 02/20 | Cut Elimination | ||
| Tue | 02/25 | Propositional Theorem Proving | HW 5 | |
| Wed | 02/26 | Rec: Sequents and KeYmaera I | code | |
| Thu | 02/27 | Inversion | ||
| Tue | 03/03 | Certifying Theorem Provers | ||
| Wed | 03/04 | Rec: Playing with proof systems | sol | |
| Thu | 03/05 | Backward Logic Programming | HW 6 | |
| Tue | 03/10 | Free: Spring break | ||
| Wed | 03/11 | Free: Spring break | ||
| Thu | 03/12 | Free: Spring break | ||
| Tue | 03/17 | Free: Optional Zoom Trial | ||
| Wed | 03/18 | Rec: Logic programming | ||
| Thu | 03/19 | Prolog | code | |
| Tue | 03/24 | Types as Predicates | HW 7 | |
| Wed | 03/25 | Rec: Programming in prolog | ||
| Thu | 03/26 | Chaining | code | |
| Tue | 03/31 | Review | HW 8 | |
| Wed | 04/01 | Rec: Pre-exam review and some more Prolog | ||
| Thu | 04/02 | Midterm II | ||
| Tue | 04/07 | Forward Logic Programming | ||
| Wed | 04/08 | Rec: Datalog | ||
| Thu | 04/09 | Unification | ||
| Tue | 04/14 | Linear Logic | HW 9 | |
| Wed | 04/15 | Rec: Linearly lining up for food | ||
| Thu | 04/16 | Linear Inversion | ||
| Tue | 04/21 | Linear Chaining | ||
| Wed | 04/22 | Rec: Focusing on linear logic | ||
| Thu | 04/23 | Substructural Operational Semantics | HW 10 | |
| Tue | 04/28 | Review | ||
| Wed | 04/29 | Rec: Practice | ||
| Thu | 04/30 | Exam Review Q&A | ||
| Fri | 05/08 | Final Exam: 5:30 | ||
Assignment Schedule
| Points | Assignment | Due | |||
|---|---|---|---|---|---|
| HW 1 | 30 | Say hi to logic | code | Tue | 01/21 |
| HW 2 | 40 | Deduce, naturally and harmoniously | code | Tue | 01/28 |
| HW 3 | 40 | Come to terms with proofs | code | Tue | 02/04 |
| HW 4 | 40 | Quantify proofs with data | code | Tue | 02/11 |
| HW 5 | 40 | Calculuate in sequents | code | Tue | 02/25 |
| HW 6 | 60 | Propositional sequent proving | code | Thu | 03/05 |
| HW 7 | 60 | G4IP and Prolog | code | Tue | 03/24 |
| HW 8 | 40 | Prolog programming | code | Tue | 03/31 |
| HW 9 | 20 | Chaining data logically | code | Tue | 04/14 |
| HW 10 | 30 | Linear blocks | code | Thu | 04/23 |
| Sum | 400 | points listed | |||
The Assignment Schedule is tentative!
Homework assignments are due on the due day.