Schedule
Sometimes, there is supplemental lecture material, but you are expected to attend and take notes.
| Date | Lecture Notes | Extra | Due |
|
| Tue | 02/02 | Overview | | |
| Wed | 02/03 | Rec: Propositions, judgements, proofs | | |
| Thu | 02/04 | Natural Deduction | | |
|
| Tue | 02/09 | Proofs as Programs | | |
| Wed | 02/10 | Rec: Proof term tutch | | |
| Thu | 02/11 | Harmony | | HW 1 |
|
| Tue | 02/16 | Verifications | | |
| Wed | 02/17 | Rec: Harmonic tutch and verifications | | |
| Thu | 02/18 | Quantification | | HW 2 |
|
| Tue | 02/23 | Free: Break day | | |
| Wed | 02/24 | Rec: Quantified tutch | | |
| Thu | 02/25 | Heyting Arithmetic | | HW 3 |
|
| Tue | 03/02 | Induction/Recursion | | |
| Wed | 03/03 | Rec: Recurse in tutch | | |
| Thu | 03/04 | Review | | HW 4 |
|
| Tue | 03/09 | ?Midterm I? | | |
| Wed | 03/10 | Rec: Judgmental natural deductions | | |
| Thu | 03/11 | Sequent Calculus | | |
|
| Tue | 03/16 | Cut Elimination | | |
| Wed | 03/17 | Rec: Sequents and cuts and KeYmaera I | | |
| Thu | 03/18 | Propositional Theorem Proving | | HW 5 |
|
| Tue | 03/23 | Inversion | | |
| Wed | 03/24 | Rec: Playing with proof systems | | |
| Thu | 03/25 | Certifying Theorem Provers | | HW 6 |
|
| Tue | 03/30 | Classical Logic | | |
| Wed | 03/31 | Rec: Classical and certified proofs | | |
| Thu | 04/01 | Review | | HW 7 |
|
| Tue | 04/06 | ?Midterm II? | | |
| Wed | 04/07 | Rec: Computation by reading proofs | | |
| Thu | 04/08 | Backward Logic Programming | | |
|
| Tue | 04/13 | Prolog | | |
| Wed | 04/14 | Rec: Programming in prolog | | HW 8 |
| Thu | 04/15 | Free: Break day | | |
|
| Tue | 04/20 | Types as Predicates | | |
| Wed | 04/21 | Rec: Moded and typed programming in prolog | | |
| Thu | 04/22 | Linear Logic | | HW 9 |
|
| Tue | 04/27 | Linear Inversion | | |
| Wed | 04/28 | Rec: Linearly lining up for food | | |
| Thu | 04/29 | Chaining | | |
|
| Tue | 05/04 | Forward Logic Programming | | |
| Wed | 05/05 | Rec: Datalog in chains | | |
| Thu | 05/06 | Review | | HW 10 |
|
| TBA | Final Exam | | |
The lecture schedule is tentative!
Assignment Schedule
| Points | Assignment | | Due |
| HW 1 | 40 | Say hi to logic | | Thu | 02/11 |
| HW 2 | 40 | Deduce, naturally and harmoniously | | Thu | 02/18 |
| HW 3 | 40 | Come to terms with proofs | | Thu | 02/25 |
| HW 4 | 40 | Quantify proofs with data | | Thu | 03/04 |
| HW 5 | 40 | Calculuate in sequents with cuts | | Thu | 03/18 |
| HW 6 | 40 | Propositional sequent proving | | Thu | 03/25 |
| HW 7 | 40 | G4IP quite classically | | Thu | 04/01 |
| HW 8 | 40 | Prolog programming | | Wed | 04/14 |
| HW 9 | 40 | Prolog proving | | Thu | 04/22 |
| HW 10 | 40 | Linear blocks | | Thu | 05/06 |
| Sum | 400 | points listed |
The Assignment Schedule is tentative!
Homework assignments are due on the due day.
