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