| Date |
Lecture |
|
|
Homework |
|
| We | Sep | 5 |
Overview/Natural Deduction |
|
|
|
| Fr | Sep | 7 |
Natural Deduction |
|
|
|
|
| Mo | Sep | 10 |
Tutorial (Maja) |
|
|
|
| We | Sep | 12 |
Tutorial (Maja) |
|
|
|
| Fr | Sep | 14 |
Normal Proofs |
|
|
HW 1 out / |
|
| Mo | Sep | 17 |
Notational definitions |
|
|
|
| We | Sep | 19 |
Proofs-as-Programs (1) |
|
|
|
| Fr | Sep | 21 |
Proofs-as-Programs |
|
|
HW 1 due / HW 2 out |
|
| Mo | Sep | 24 |
Properties of proof terms |
|
|
|
| We | Sep | 26 |
Lambda-calculus |
|
|
|
| Fr | Sep | 28 |
Primitive recursion |
|
|
HW 2 due / HW 3 out |
|
| Mo | Oct | 1 |
Data-types |
|
|
|
| We | Oct | 3 |
Induction |
|
|
|
| Fr | Oct | 5 |
to be announced
|
|
|
HW 3 due / HW 4 out |
|
| Mo | Oct | 8 |
Thanksgiving Holiday |
|
|
|
| Tu | Oct | 9 |
First-order logic |
|
|
|
| We | Oct | 10 |
First-order logic |
|
|
|
| Fr | Oct | 12 |
First-order logic |
|
|
HW 4 due / HW 5 out |
|
| Mo | Oct | 15 |
Contracting proofs |
|
|
|
| We | Oct | 17 |
Reasoning about data |
|
|
|
| Fr | Oct | 19 |
Review |
|
|
HW 5 due |
|
| Mo | Oct | 22 |
Midterm |
|
|
|
| We | Oct | 24 |
Normal natural deduction |
|
|
|
| Fr | Oct | 26 |
Consistency |
|
|
|
|
| Mo | Oct | 29 |
Sequent Calculus |
|
|
|
| We | Oct | 31 |
Meta-theoretic properties |
|
|
|
| Fr | Nov | 2 |
Inversion and focusing |
|
|
Project Proposal due |
|
| Mo | Nov | 5 |
Guided theorem prover |
|
|
|
| We | Nov | 7 |
Logic Programming |
|
|
|
| Fr | Nov | 9 |
Logic Programming |
|
|
|
|
| Mo | Nov | 12 |
Forward theorem proving |
|
|
|
| We | Nov | 14 |
Forward theorem proving |
|
|
|
| Fr | Nov | 16 |
Bi-directional theorem proving |
|
|
Project Milestone |
|
| Mo | Nov | 19 |
Special topic: Modal logic |
|
|
|
| We | Nov | 21 |
Special topic: Dependent types |
|
|
|
| Fr | Nov | 23 |
Special topic: Linear logic |
|
|
|
|
| Mo | Nov | 26 |
Presentations |
|
|
|
| We | Nov | 28 |
Presentations |
|
|
|
| Fr | Nov | 30 |
Presentations |
|
|
|
|
| Mo | Dec | 3 |
Presentations |
|
|
|
|