| Date |
Lecture |
|
|
Homework |
|
| Fr | Sep | 2 |
Overview |
|
|
|
|
| Mo | Sep | 5 |
Labour Day |
|
|
|
| We | Sep | 7 |
Natural Deduction |
|
|
HW1 out |
| Fr | Sep | 9 |
Natural Deduction |
|
|
|
|
| Mo | Sep | 12 |
Notational definitions |
|
|
|
| We | Sep | 14 |
Bi-directional natural deduction |
|
|
|
| Fr | Sep | 16 |
Bi-directional natural deduction |
|
|
|
|
| Mo | Sep | 19 |
Sequent Calculus |
|
|
|
| We | Sep | 21 |
Sequent Calculus |
|
|
HW1 due / HW2 out |
| Fr | Sep | 23 |
Sequent Calculus |
|
|
|
|
| Mo | Sep | 26 |
Introduction to SML |
|
|
|
| We | Sep | 28 |
A guided propositional theorem prover |
|
|
|
| Fr | Sep | 30 |
Inversion and Focusing
|
|
|
|
|
| Mo | Oct | 3 |
Curry-Howard Isomorphism |
|
|
|
| We | Oct | 5 |
Lambda-Calculus |
|
|
HW2 due/ HW3 out |
| Fr | Oct | 7 |
Lambda-Calculus |
|
|
|
|
| Mo | Oct | 10 |
Thanksgiving |
|
|
|
| We | Oct | 12 |
Proof terms |
|
|
|
| Fr | Oct | 14 |
Proof (Type) checking |
|
|
|
|
| Mo | Oct | 17 |
Quantification |
|
|
|
| We | Oct | 19 |
Quantification |
|
|
HW 3 due |
| Fr | Oct | 21 |
Quantification |
|
|
|
|
| Mo | Oct | 24 |
Review |
|
|
|
| We | Oct | 26 |
No Class |
|
|
|
| Fr | Oct | 28 |
Midterm |
|
|
|
|
| Mo | Oct | 31 |
Propositional theorem proving |
|
|
|
| We | Nov | 2 |
Dyckhoff's procedure |
|
|
HW4 out |
| Fr | Nov | 4 |
Stalmarck |
|
|
|
|
| Mo | Nov | 7 |
Loop-detection in propositional logic |
|
|
|
| We | Nov | 9 |
Redundancy elimination |
|
|
|
| Fr | Nov | 11 |
Redundancy elimination |
|
|
|
|
| Mo | Nov | 14 |
First-order theorem proving |
|
|
|
| We | Nov | 16 |
Unification |
|
|
HW4 due / HW5 out |
| Fr | Nov | 18 |
Unification |
|
|
|
|
| Mo | Nov | 21 |
Logic Programming |
|
|
|
| We | Nov | 23 |
Logic Programming |
|
|
|
| Fr | Nov | 25 |
Logic Programming |
|
|
|
|
| Mo | Nov | 28 |
Higher-order logic programming |
|
|
|
| We | Nov | 30 |
Higher-order logic programming |
|
|
HW5 due |
| Th | Dec | 1 |
Higher-order logic programming |
|
|
|
| Fr | Dec | 2 |
Higher-order logic programming |
|
|
|
|
| Mo | Dec | 5 |
Review |
|
|
|