Inhalt
Die Lehrveranstaltung gibt eine Einführung in den Beweisassistenten Isabelle/HOL.
Zeitplan
Die Vorlesung wird geblockt abgehalten. Statt einer wöchentlichen 1-stündigen Vorlesung, finden 4 Sessions zu je 3 Stunden statt. Kurse, die einige der in der VO besprochenen Inhalte vertiefen, sind in Klammern aufgeführt.
| Session | Datum | Themen | Folien | Quelltext |
|---|---|---|---|---|
| 1 | 11.03. | formal verification, Isabelle/HOL basics, functional programming in HOL (functional programming) | pdf (4x1) | Archiv |
| 2 | 25.03 | simplification (term rewriting), function definitions, induction, calculational reasoning | pdf (4x1) | Archiv |
| 3 | 01.04. | natural deduction, propositional logic, predicate logic (logic) | pdf (4x1) | Archiv |
| 4 | 15.04. | (inductively defined) sets, relations, advanced topics | pdf (4x1) | Archiv |
