15-317: Constructive Logic (Fa'16)

Schedule

There may be occasional supplemental handouts on lecture material, but you are expected to attend and take notes.

Date		Lecture Notes	Extra	Due
Tue	08/30	Overview
Wed	08/31	Rec: Propositions, judgements, proofs	code
Thu	09/01	Natural Deduction
Tue	09/06	Harmony		HW 0
Wed	09/07	Rec: Harmonic tutch
Thu	09/08	Classical Logic
Tue	09/13	Proofs as Programs		HW 1
Wed	09/14	Rec: Proof terms and verifications	code
Thu	09/15	Quantification
Tue	09/20	Natural Numbers		HW 2
Wed	09/21	Rec: Recurse and arithmetic in tutch
Thu	09/22	Sequent Calculus
Tue	09/27	Review		HW 3
Wed	09/28	Rec: Natural deductions versus sequents
Thu	09/29	Midterm I
Tue	10/04	Cut Elimination
Wed	10/05	Rec: Sequents and KeYmaera I	code
Thu	10/06	Inversion
Tue	10/11	Propositional Theorem Proving	extra	HW 4
Wed	10/12	Rec: Playing with proof systems	sol
Thu	10/13	Quantifiers: Cut and Dependent Types	2.6,4.8
Tue	10/18	Backward Logic Programming	code	HW 5
Wed	10/19	Rec: Quantifiers and logic programming
Thu	10/20	Prolog	code
Tue	10/25	Prolog Programming Techniques	code	HW 6
Wed	10/26	Rec: Programming in prolog	code
Thu	10/27	Operational Semantics	more
Tue	11/01	Unification		HW 7
Wed	11/02	Rec: Prolog techniques, semantics, and unification	code
Thu	11/03	Unification Resolution	extra
Tue	11/08	Review		HW 8
Wed	11/09	Rec: Pre-exam review and some more Prolog	code
Thu	11/10	Midterm II
Tue	11/15	Forward Logic Programming	code	HW 8½
Wed	11/16	Rec: Unified logic programs forward
Thu	11/17	Forward Computation	code
Tue	11/22	Free: Optional: Resolution
Wed	11/23	Free: Thanksgiving break
Thu	11/24	Free: Thanksgiving break
Tue	11/29	Linear Logic
Wed	11/30	Rec: Linearly lining up for food
Thu	12/01	Linear Focusing	more	HW 9
Tue	12/06	Substructural Operational Semantics
Wed	12/07	Rec: Exam review
Thu	12/08	Review		HW 10
Fri	12/16	Final Exam

The lecture schedule is tentative!

Assignment Schedule

	Points	Assignment		Due
HW 0	10	Say hi to logic	code	Tue	09/06
HW 1	40	Deduce, naturally and harmoniously	code	Tue	09/13
HW 2	40	Come to terms with proofs	code	Tue	09/20
HW 3	40	Quantify proofs with data	code	Tue	09/27
HW 4	40	Calculuate in sequents	code	Tue	10/11
HW 5	40	Propositional theorem proving	code	Tue	10/18
HW 6	40	Sequential quantifiers and being logical about programming	code	Tue	10/25
HW 7	40	Practicing prolog programming	code	Tue	11/01
HW 8	20	Programming logically	code	Tue	11/08
HW 8½	20	Programming more logically	code	Tue	11/15
HW 9	40	Forward logic programming		Thu	12/01
HW 10	30	Let's be linear	code	Thu	12/08
Sum	400	points listed

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