|
Date
|
Topic
|
Readings
|
Lab
|
Assignment due
|
Other
|
| T |
Sep 24 |
Basic ideas of Theorem Proving |
|
|
|
|
| Th |
26 |
Propositional Logic, Gentzen's Natural Deduction |
LACI ch. 1 |
|
|
|
| T |
Oct 1 |
Propositional II |
LACI 2.1 - 2.3 |
|
|
|
| Th |
3 |
Propositional III |
LACI 2.4 - 2.6 |
|
|
|
| T |
8 |
Propositional IV |
LACI 2.7 - 2.10 |
|
A1 due
|
|
| Th |
10 |
Predicate I |
LACI 3 - 3.2.1 |
|
|
|
| T |
15 |
Predicate II |
LACI 3.2.2 - 3.2.5 |
|
|
|
| Th |
17 |
Predicate III |
LACI 3.2.6 - 3.2.9 |
|
A2 due
|
|
| T |
22 |
Equality, Natural numbers |
|
|
|
|
| Th |
24 |
Natural number theorems in Lean |
|
|
|
|
| T |
29 |
Intro to Agda, equality and naturals |
|
|
|
|
| Th |
31 |
Agda numeric fundamentals |
|
|
|
|
| T |
Nov 5 |
TBA |
|
|
|
|
| W |
6 |
|
|
|
A3 due
|
|
| Th |
7 |
TBA |
|
|
|
|
| T |
12 |
TBA |
|
|
|
|
| Th |
14 |
TBA |
|
|
|
|
| T |
19 |
TBA |
|
|
A6 (tba) |
|
| Th |
21 |
TBA |
|
|
|
|
| T |
26 |
Fall Break |
|
|
|
|
| Th |
28 |
Fall Break |
|
|
|
|
| T |
Dec 3 |
TBA |
|
|
|
|
| Th |
5 |
TBA |
|
|
A7 (tba) |
|