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