Description
The course discusses different proof systems for first-order logic (without equality) as well as limitations and extensions of first-order logic: semantic tableaux, sequent calculus, Hilbert systems; soundness and completeness; compactness; Herbrand's theorem; Craig's interpolation theorem; second-order logic; Curry-Howard isomorphism.
Schedule
| week | date | slides | exercises | solutions | remarks |
|---|---|---|---|---|---|
| 1 | 03.03 | pdf (1, 4) | |||
| 2 | 10.03 | pdf (1, 4) | |||
| 3 | 17.03 | pdf (1, 4) | |||
| 4 | 24.03 | pdf (1, 4) | |||
| 5 | 31.03 | pdf (1, 4) | |||
| 6 | 21.04 | pdf (1, 4) | |||
| 7 | 28.04 | pdf (1, 4) | |||
| 8 | 05.05 | ||||
| 9 | 12.05 | exam |