15-317: Constructive Logic (Sp'20)

Schedule

Sometimes, there is supplemental lecture material, but you are expected to attend and take notes.
DateLecture NotesExtraDue
Tue01/14Overview
Wed01/15Rec: Propositions, judgements, proofs
Thu01/16Natural Deduction
Tue01/21Proofs as ProgramsHW 1 
Wed01/22Rec: Proof term tutchcode 
Thu01/23Harmony
Tue01/28VerificationsHW 2 
Wed01/29Rec: Harmonic tutch and verifications
Thu01/30Quantification
Tue02/04Induction/RecursionHW 3 
Wed02/05Rec: Recurse in tutch
Thu02/06Heyting Arithmetic
Tue02/11ReviewHW 4 
Wed02/12Rec: Practice
Thu02/13Midterm I
Tue02/18Sequent Calculus
Wed02/19Rec: Natural deductions versus sequents
Thu02/20Cut Elimination
Tue02/25Propositional Theorem ProvingHW 5 
Wed02/26Rec: Sequents and KeYmaera I
Thu02/27Inversion
Tue03/03Certifying Theorem ProversHW 6 
Wed03/04Rec: Playing with proof systems
Thu03/05Backward Logic Programming
Tue03/10Free: Spring breakHW 7 
Wed03/11Free: Spring break
Thu03/12Free: Spring break
Tue03/17PrologHW 8 
Wed03/18Rec: Quantifiers and logic programming
Thu03/19Types as Predicates
Tue03/24ChainingHW 9 
Wed03/25Rec: Programming in prolog
Thu03/26Unification
Tue03/31Review
Wed04/01Rec: Prolog techniques, semantics, and unification
Thu04/02Midterm II
Tue04/07Unification Resolution
Wed04/08Rec: Pre-exam review and some more Prolog
Thu04/09Forward Logic ProgrammingHW 10 
Tue04/14Focusing
Wed04/15Rec: TBD
Thu04/16Free: Spring Carnival
Tue04/21Linear Logic
Wed04/22Rec: Linearly lining up for food
Thu04/23Linear FocusingHW 11 
Tue04/28TBD
Wed04/29Rec: Exam review
Thu04/30Review
Final Exam
The lecture schedule is tentative!

Assignment Schedule

PointsAssignmentDue
HW 130Say hi to logiccodeTue01/21
HW 240Deduce, naturally and harmoniouslycodeTue01/28
HW 340Come to terms with proofsTue02/04
HW 440Quantify proofs with dataTue02/11
HW 540Calculuate in sequentsTue02/25
HW 640Propositional theorem provingTue03/03
HW 740Sequential quantifiers and being logical about programmingTue03/10
HW 840Practicing prolog programmingTue03/17
HW 930Programming logicallyTue03/24
HW 1040Forward logic programmingThu04/09
HW 1120Let's be linearThu04/23
Sum400points listed

The Assignment Schedule is tentative!
Homework assignments are due on the due day.