Lectures and classes will take place in room 1311, if nothing else is indicated. "Academic quarter" will be applied below, 8-10 thus means 8.15 - 10.00.
| # | Date | Time | Text | Subject |
| 1 | Mo 22/3 | 8-10 | L 2.4 | Semantics of predicate logic: Undecidability results. |
| 2 | Tu 23/3 | 15-17 | L 2.5, E 1.1 | Provability in predicate logic: Undecidability results. Equational logic: completeness, proof search. |
| 3 | Th 25/3 | 8-10 | E 1.1-2 | Equational logic: undecidability and decidability. The term model. Unification and matching. |
| 4 | Fr 26/3 | 8-10 | X 1 | Exercise class. Tarski's quantifier elimination theorem and some applications. |
| 5 | Mo 29/3 | 13-15 room 6140 |
(FD) | |
| 6 | Tu 30/3 | 8-10 | (FD) | |
| 7 | Tu 13/4 | 10-12 room 1254 |
(FD) | |
| 8 | Th 15/4 | 13-15 | (FD) | |
| 9 | Tu 20/4 | 8-10 | (FD) | |
| 10 | Th 22/4 | 8-10 | (FD) | |
| 11 | Mo 26/4 | 8-10 | C 10 | Distributive lattices, Heyting algebras. Soundness and completeness for intuitionistic propositional logic. |
| 12 | Th 29/4 | 10-12 room 1211 |
C 10, F II | Soundness and completeness for intuitionistic propositional logic (cont.) The tableau method for classical propositional logic. |
| 13 | Mo 3/5 | 10-12 | F IV - V | The tableau method for classical predicate logic. Gödel's completeness theorem. |
| 14 | Tu 4/5 | 8-10 | F V, R | Completeness (cont.). Resolution method. The Otter system and examples. |
| 15 | Th 6/5 | 8-10 4407 |
Laborative exercise in Agda/Alfa (FD) | |
| 16 | Fr 7/5 | 13-15 | R, X 3 | Resolution (cont.). Exercise class. |
| 17 | Mo 10/5 | 8-10 | L 3.1-3.4 | Model-checking, CTL-logic and semantical equivalences. |
| 18 | Tu 11/5 | 13-15 | L 3.5, 6.1 | Labelling algorithm for CTL-logic. Examples. Binary decision diagrams. |
| 19 | Th 13/5 | 13-15 | L 6.2, X 4 | Ordered binary decision diagrams. Reduced and canonical forms. Exercise class. |
Tentamen (exam): May 26.