15-317: Constructive Logic (Fa'16)


There may be occasional supplemental handouts on lecture material, but you are expected to attend and take notes.
DateLecture NotesExtraDue
Wed08/31Rec: Propositions, judgements, proofscode 
Thu09/01Natural Deduction
Tue09/06HarmonyHW 0 
Wed09/07Rec: Harmonic tutch
Thu09/08Classical Logic
Tue09/13Proofs as ProgramsHW 1 
Wed09/14Rec: Proof terms and verificationscode 
Tue09/20Natural NumbersHW 2 
Wed09/21Rec: Recurse and arithmetic in tutch
Thu09/22Sequent Calculus
Tue09/27ReviewHW 3 
Wed09/28Rec: Natural deductions versus sequents
Thu09/29Midterm I
Tue10/04Cut Elimination
Wed10/05Rec: Sequents and KeYmaera Icode 
Tue10/11Propositional Theorem Proving(NextraHW 4 
Wed10/12Rec: Playing with proof systemssol
Thu10/13Quantifiers: Cut and Dependent Types(N2.6,4.8
Tue10/18Backward Logic Programming(Ncode HW 5 
Wed10/19Rec: Quantifiers and logic programming
Tue10/25Prolog Programming Techniquescode HW 6 
Wed10/26Rec: Programming in prologcode 
Thu10/27Operational Semantics(Nmore
Tue11/01Unification(NHW 7 
Wed11/02Rec: Prolog techniques, semantics, and unificationcode 
Thu11/03Unification Resolution(Nextra
Tue11/08ReviewHW 8 
Wed11/09Rec: Pre-exam review and some more Prologcode 
Thu11/10Midterm II
Tue11/15Forward Logic Programmingcode HW 8½ 
Wed11/16Rec: Unified logic programs forward
Thu11/17Forward Computationcode 
Tue11/22Free: Optional: Resolution(N
Wed11/23Free: Thanksgiving break
Thu11/24Free: Thanksgiving break
Tue11/29Linear Logic(N
Wed11/30Rec: Linearly lining up for food
Thu12/01Linear Focusing(NmoreHW 9 
Tue12/06Substructural Operational Semantics(N
Wed12/07Rec: Exam review
Thu12/08Review(NHW 10 
Fri12/16Final Exam
The lecture schedule is tentative!

Assignment Schedule

HW 010Say hi to logiccode,solTue 09/06
HW 140Deduce, naturally and harmoniouslycode,solTue 09/13
HW 240Come to terms with proofscode,solTue 09/20
HW 340Quantify proofs with datacode,solTue 09/27
HW 440Calculuate in sequentscodeTue 10/11
HW 540Propositional theorem provingcode,solTue 10/18
HW 640Sequential quantifiers and being logical about programmingcode,solTue 10/25
HW 740Practicing prolog programmingcode,solTue 11/01
HW 820Programming logicallycode,solTue 11/08
HW 8½20Programming more logicallycodeTue 11/15
HW 940Forward logic programmingcodeThu 12/01
HW 1030Let's be linearcodeThu 12/08
Sum400points listed

The Assignment Schedule is tentative!
Homework assignments are due at start of lecture on the due day.