Introduction
The lecture is blocked. Instead of a weekly 1-hour lecture, there will be 4 sessions of 3 hours each. Related courses to some of the discussed topics are given in parentheses.
| session 1: | formal verification, Isabelle/HOL basics, functional programming in HOL (functional programming) |
| session 2: | simplification (term rewriting), function definitions, induction, calculational reasoning |
| session 3: | natural deduction, propositional logic, predicate logic (logic) |
| session 4: | (inductively defined) sets, relations, advanced topics |