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 |
28 |
Overview |
|
|
| Wed |
Aug |
30 |
Natural Deduction |
|
HW1 out |
|
| Mon |
Sep |
4 |
No class |
|
|
| Wed |
Sep |
6 |
Harmony |
|
HW1 due, HW2 out |
|
| Mon |
Sep |
11 |
Proofs as Programs |
|
|
| Wed |
Sep |
13 |
Verifications and Uses |
|
HW2 due, HW3 out |
|
| Mon |
Sep |
18 |
Quantification |
|
| Wed |
Sep |
20 |
Heyting Arithmetic |
|
HW3 due, HW4 out |
|
| Mon |
Sep |
25 |
Sequent Calculus |
|
|
| Wed |
Sep |
27 |
Sequent Calculus |
|
HW4 due, HW5 out |
|
| Mon |
Oct |
2 |
Midterm 1 |
|
|
| Wed |
Oct |
4 |
Cut Elimination |
|
HW5 due, HW6 out |
|
| Mon |
Oct |
9 |
Propositional Theorem Proving |
|
|
| Wed |
Oct |
11 |
Inversion |
|
HW6 due, HW7 out |
|
| Mon |
Oct |
16 |
No class |
|
|
| Wed |
Oct |
18 |
No class |
|
|
|
| Mon |
Oct |
23 |
Classical Logic |
|
|
| Wed |
Oct |
25 |
Logic Programming |
|
HW7 due, HW8 out |
|
| Mon |
Oct |
30 |
Prolog |
|
|
| Wed |
Nov |
1 |
Backward Chaining |
|
HW8 due, HW9 out |
|
| Mon |
Nov |
6 |
Forward Chaining |
|
|
| Wed |
Nov |
8 |
Linear Logic |
(Blocks World, Substructural Deduction) |
HW9 due, HW10 out |
|
| Mon |
Nov |
13 |
Midterm 2 |
|
|
| Wed |
Nov |
15 |
Focusing |
|
HW10 due, HW11 out |
|
| Mon |
Nov |
20 |
Modal Logic |
|
|
| Wed |
Nov |
22 |
No class |
|
|
|
| Mon |
Nov |
27 |
Ordered Logic |
|
|
| Wed |
Nov |
29 |
Session Types |
|
|
| Fri |
Dec |
1 |
|
|
HW12 due |
|
| Mon |
Dec |
4 |
Classical Sequent Calculus |
|
|
| Wed |
Dec |
6 |
TBA |
|
|
|
| TBA |
|
|
Final exam |
|
|
[ Home
| Schedule
| Assignments
| Software
]
|