15-317: Constructive Logic (Sp'21)

Schedule

Sometimes, there is supplemental lecture material, but you are expected to attend and take notes.

Date		Lecture Notes	Extra	Due
Tue	02/02	Overview
Wed	02/03	Rec: Propositions, judgements, proofs
Thu	02/04	Natural Deduction
Tue	02/09	Proofs as Programs
Wed	02/10	Rec: Proof term proofs
Thu	02/11	Harmony		HW 1
Tue	02/16	Verifications
Wed	02/17	Rec: Harmonic proofs and verifications
Thu	02/18	Quantification		HW 2
Tue	02/23	Free: Break day
Wed	02/24	Rec: Quantified proofs
Thu	02/25	Heyting Arithmetic		HW 3
Tue	03/02	Induction/Recursion	code
Wed	03/03	Rec: Recurse in proofs
Thu	03/04	Review		HW 4
Tue	03/09	Midterm I
Wed	03/10	Rec: Judgmental natural deductions
Thu	03/11	Sequent Calculus
Tue	03/16	Cut Elimination
Wed	03/17	Rec: Sequents and cuts and sequent proofs
Thu	03/18	Propositional Theorem Proving		HW 5
Tue	03/23	Inversion
Wed	03/24	Rec: Playing with proof systems
Thu	03/25	Certifying Theorem Provers		HW 6
Tue	03/30	Focusing
Wed	03/31	Rec: Focused and certified proofs
Thu	04/01	Review
Tue	04/06	Midterm II
Wed	04/07	Rec: Freestyle Clogic Magic
Thu	04/08	Backward Logic Programming	code
Tue	04/13	Prolog	code	HW 7
Wed	04/14	Rec: Programming in prolog	code
Thu	04/15	Free: Carnival
Tue	04/20	Types as Predicates
Wed	04/21	Rec: Moded and typed programming in prolog
Thu	04/22	Chaining	code	HW 8
Tue	04/27	Forward Logic Programming
Wed	04/28	Rec: Datalog in chains	code
Thu	04/29	Linear Logic
Tue	05/04	Linear Inversion
Wed	05/05	Rec: Linearly lining up for food
Thu	05/06	Review		HW 9
Tue	05/11	Final Exam 8:30am-11:30am

The lecture schedule is tentative!

Assignment Schedule

Assignments are released on Gradescope.

	Points	Assignment		Due
HW 1	20	Say hi to logic	code	Thu	02/11
HW 2	40	Come to terms with proofs	code	Thu	02/18
HW 3	40	Deduce, naturally and harmoniously	code	Thu	02/25
HW 4	40	Quantify proofs with data	code	Thu	03/04
HW 5	40	Calculuate in sequents with cuts	code	Thu	03/18
HW 6	50	Propositional sequent proving	code	Thu	03/25
HW 7	80	G4IP quite classically	code	Tue	04/13
HW 8	40	Prolog programming and proving	code	Thu	04/22
HW 9	50	Datalog and linear blocks	code	Thu	05/06
Sum	400	points listed

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