15-317 Constructive Logic
Schedule

The class notes provide additional reading material. They complement the lecture, but do not replace it.
The schedule (including exam dates) is subject to change throughout the semester.

Date			Lecture or Recitation	Additional Material	Homework Due/Out

Mon	Aug	29	Overview
Tue	Aug	30	Recitation
Wed	Aug	31	Natural Deduction		HW1 out

Mon	Sep	5	No class
Tue	Sep	6	Recitation
Wed	Sep	7	Harmony		HW1 due, HW2 out

Mon	Sep	12	Proofs as Programs
Tue	Sep	13	Recitation: Proofs as ML programs
Wed	Sep	14	Verifications and Uses		HW2 due, HW3 out

Mon	Sep	19	Quantification
Tue	Sep	20	Recitation
Wed	Sep	21	Heyting Arithmetic		HW3 due, HW4 out

Mon	Sep	26	Sequent Calculus
Tue	Sep	27	Recitation: Admissibility and derivability
Wed	Sep	28	Sequent Calculus		HW4 due, HW5 out

Mon	Oct	3	Midterm 1
Tue	Oct	4	Recitation: Midterm review
Wed	Oct	5	Cut Elimination		HW5 due, HW6 out

Mon	Oct	10	Classical Logic
Tue	Oct	11	Recitation: Kolmogorov translation
Wed	Oct	12	Propositional Theorem Proving		HW6 due, HW7 out

Mon	Oct	17	No class
Tue	Oct	18	No recitation
Wed	Oct	19	No class

Mon	Oct	24	Inversion
Tue	Oct	25	Recitation
Wed	Oct	26	Logic Programming		HW7 due, HW8 out

Mon	Oct	31	Prolog
Tue	Nov	1	Recitation: Practical Prolog
Wed	Nov	2	Backward Chaining		HW8 due, HW9 out

Mon	Nov	7	Midterm 2
Tue	Nov	8	Recitation: Midterm review
Wed	Nov	9	Linear Logic	(Blocks World, Substructural Deduction)	HW9 due, HW10 out

Mon	Nov	14	Forward Chaining
Tue	Nov	15	Recitation
Wed	Nov	16	Focusing		HW10 due, HW11 out

Mon	Nov	21	Modal Logic
Tue	Nov	22	Recitation: Linear logic applications		HW11 due, HW12 out
Wed	Nov	23	No class

Mon	Nov	28	Ordered Logic
Tue	Nov	29	Recitation: Lax logic and monads
Wed	Nov	30	Session Types
Fri	Dec	2			HW12 due

Mon	Dec	5	Certifying Theorem Provers
Tue	Dec	6	Recitation
Wed	Dec	7	TBA

Mon	Dec	12	Final exam

[ Home | Schedule | Assignments | Software ]