15-317: Constructive Logic (Sp'21)


Sometimes, there is supplemental lecture material, but you are expected to attend and take notes.
DateLecture NotesExtraDue
Wed02/03Rec: Propositions, judgements, proofs
Thu02/04Natural Deduction
Tue02/09Proofs as Programs
Wed02/10Rec: Proof term tutch
Thu02/11HarmonyHW 1 
Wed02/17Rec: Harmonic tutch and verifications
Thu02/18QuantificationHW 2 
Tue02/23Free: Break day
Wed02/24Rec: Quantified tutch
Thu02/25Heyting ArithmeticHW 3 
Wed03/03Rec: Recurse in tutch
Thu03/04ReviewHW 4 
Tue03/09?Midterm I?
Wed03/10Rec: Judgmental natural deductions
Thu03/11Sequent Calculus
Tue03/16Cut Elimination
Wed03/17Rec: Sequents and cuts and KeYmaera I
Thu03/18Propositional Theorem ProvingHW 5 
Wed03/24Rec: Playing with proof systems
Thu03/25Certifying Theorem ProversHW 6 
Tue03/30Classical Logic
Wed03/31Rec: Classical and certified proofs
Thu04/01ReviewHW 7 
Tue04/06?Midterm II?
Wed04/07Rec: Computation by reading proofs
Thu04/08Backward Logic Programming
Wed04/14Rec: Programming in prologHW 8 
Thu04/15Free: Break day
Tue04/20Types as Predicates
Wed04/21Rec: Moded and typed programming in prolog
Thu04/22Linear LogicHW 9 
Tue04/27Linear Inversion
Wed04/28Rec: Linearly lining up for food
Tue05/04Forward Logic Programming
Wed05/05Rec: Datalog in chains
Thu05/06ReviewHW 10 
TBAFinal Exam
The lecture schedule is tentative!

Assignment Schedule

HW 140Say hi to logicThu02/11
HW 240Deduce, naturally and harmoniouslyThu02/18
HW 340Come to terms with proofsThu02/25
HW 440Quantify proofs with dataThu03/04
HW 540Calculuate in sequents with cutsThu03/18
HW 640Propositional sequent provingThu03/25
HW 740G4IP quite classicallyThu04/01
HW 840Prolog programmingWed04/14
HW 940Prolog provingThu04/22
HW 1040Linear blocksThu05/06
Sum400points listed

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