15-317: Constructive Logic (Fa'16)


There may be occasional supplemental handouts on lecture material, but you are expected to attend and take notes.
Tue 08/30Overview
Wed 08/31Rec: Propositions, judgements, proofscode 
Thu 09/01Natural Deduction
Tue 09/06HarmonyHW 0 
Wed 09/07Rec: Harmonic tutch
Thu 09/08Classical Logic
Tue 09/13Proofs as ProgramsHW 1 
Wed 09/14Rec: Proof terms and verificationscode 
Thu 09/15Quantification
Tue 09/20Natural NumbersHW 2 
Wed 09/21Rec: Recurse and arithmetic in tutch
Thu 09/22Sequent Calculus
Tue 09/27ReviewHW 3 
Wed 09/28Rec: Natural deductions versus sequents
Thu 09/29Midterm I
Tue 10/04Cut Elimination
Wed 10/05Rec: Sequents and KeYmaera Icode 
Thu 10/06Inversion
Tue 10/11Propositional Theorem Proving(NextraHW 4 
Wed 10/12Rec: Playing with proof systemssol
Thu 10/13Quantifiers: Cut and Dependent Types(N2.6,4.8
Tue 10/18Backward Logic Programming(Ncode HW 5 
Wed 10/19Rec: Quantifiers and logic programming
Thu 10/20Prologcode 
Tue 10/25Prolog Programming Techniquescode HW 6 
Wed 10/26Rec: Programming in prologcode 
Thu 10/27Unification
Tue 11/01Unification ResolutionHW 7 
Wed 11/02Rec: G4ip in prolog, review
Thu 11/03Operational Semantics
Tue 11/08Review
Wed 11/09Rec: Growing trees and substituting blocks in Prolog
Thu 11/10Midterm II
Tue 11/15Forward Logic Programming
Wed 11/16Rec: Unified logic programs forwardHW 8 
Thu 11/17Forward Computation
Tue 11/22Optional: Exam-Problem-Solving Session
Wed 11/23Thanksgiving break
Thu 11/24Thanksgiving break
Tue 11/29Linear Logic
Wed 11/30Rec: Linearly forward
Thu 12/01Linear FocusingHW 9 
Tue 12/06Substructural Operational Semantics
Wed 12/07Rec: Exam review
Thu 12/08Exam reviewHW 10 
Fri 12/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 provingcodeTue 10/18
HW 640Sequential quantifiers and being logical about programmingcodeTue 10/25
HW 740Inversion for proof searchcodeTue 11/01
HW 840Programming logicallyWed 11/16
HW 940Forward-looking prologThu 12/01
HW 1030Linearized logic and logical linearitiesThu 12/08
Sum400points listed

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