15-317 Constructive Logic

  • The class notes provide additional reading material.
    They complement, but do not replace the lecture.
  • The schedule is subject to change throughout the semester.
Date Lecture or Recitation Additional Material Homework Out/Due

Mon Aug 26 Overview
Wed Aug 28 Natural Deduction

Mon Sep 2 Labor Day Holiday
Wed Sep 4 Harmony

Mon Sep 9 Proofs as Programs
Wed Sep 11 Verifications

Mon Sep 16 Quantification
Wed Sep 18

Mon Sep 23 Heyting Arithmetic
Wed Sep 25 Sequent Calculus

Mon Sep 30 Midterm I practice midterm 1 practice midterm 2
Wed Oct 2 Cut Elimination

Mon Oct 7 Classical Logic
Wed Oct 9 Propositional Theorem Proving

Mon Oct 14 Inversion
Wed Oct 16 Certifying Theorem Provers

Mon Oct 21 Logic Programming
Wed Oct 23 Prolog examples

Mon Oct 28 Backward Chaining meta-interpreter
Wed Oct 30 Forward Chaining

Mon Nov 4 Focusing rule summary
Wed Nov 6 Midterm II practice midterm

Mon Nov 11 Substructural Deduction notes on linear logic
Wed Nov 13 Ordered Logic

Mon Nov 18 Modal Logic further reading
Wed Nov 20 Subsingleton Logic

Mon Nov 25 Ordered Proofs as Concurrent Programs (not covered) Homework 11 Due
Wed Nov 27 Day before Thanksgiving (no class)

Mon Dec 2 Edinburgh Logical Framework (LF)
Wed Dec 4 LF

Mon Dec 9 Final 5:30pm-8:30pm, WEH 7500 practice

[ Home | Schedule | Assignments | Software ]

Siva Somayyajula