Content
The course provides an introduction to the proof assistant Isabelle/HOL.
Schedule
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 | date | topics | slides | sources |
|---|---|---|---|---|
| 1 | 11.03. | formal verification, Isabelle/HOL basics, functional programming in HOL (functional programming) | pdf (4x1) | archive |
| 2 | 25.03 | simplification (term rewriting), function definitions, induction, calculational reasoning | pdf (4x1) | archive |
| 3 | 01.04. | natural deduction, propositional logic, predicate logic (logic) | pdf (4x1) | archive |
| 4 | 15.04. | (inductively defined) sets, relations, advanced topics | pdf (4x1) | archive |
