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/04Heyting ArithmeticHW 3 
Wed02/05Rec: Recurse in tutch
Thu02/06Induction/Recursioncode 
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 Icode 
Thu02/27Inversion
Tue03/03Certifying Theorem Provers
Wed03/04Rec: Playing with proof systemssol
Thu03/05Backward Logic ProgrammingHW 6 
Tue03/10Free: Spring break
Wed03/11Free: Spring break
Thu03/12Free: Spring break
Tue03/17Free: Optional Trial: Canvas->15317->Zoom
Wed03/18Rec: Logic programming
Thu03/19Prologcode 
Tue03/24Types as PredicatesHW 7 
Wed03/25Rec: Programming in prolog
Thu03/26Chainingcode 
Tue03/31ReviewHW 8 
Wed04/01Rec: Pre-exam review and some more Prolog
Thu04/02Midterm II
Tue04/07Forward Logic Programming
Wed04/08Rec: Datalogcode 
Thu04/09Forward Logic Programming 2 + Unification
Tue04/14TBDHW 9 
Wed04/15Rec: TBD
Thu04/16TBD
Tue04/21FocusingHW 10 
Wed04/22Rec: 
Thu04/23Linear Logic
Tue04/28Linear Focusing
Wed04/29Rec: Linearly lining up for food
Thu04/30Review
TBDFinal 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 proofscodeTue02/04
HW 440Quantify proofs with datacodeTue02/11
HW 540Calculuate in sequentscodeTue02/25
HW 660Propositional sequent provingcodeThu03/05
HW 760G4IP and PrologcodeTue03/24
HW 840Prolog programmingcodeTue03/31
HW 930Chaining data logicallycodeTue04/14
HW 1040Forward logic programmingTue04/21
Sum420points listed

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