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 | remarks |
|---|---|---|---|---|
| 1 | 06.03 | |||
| 2 | 13.03 | |||
| 3 | 20.03 | (slides modified) | ||
| 4 | 27.03 | |||
| 5 | 03.04 | |||
| 6 | 24.04 | |||
| 7 | 08.05 | exam |