Inhalt
- Einführung in die axiomatische Mengenlehre als Fundament für alle mengenbasierten Spezifikationssprachen.
- Einführung in die modale Logik als Grundlage für alle Zustandsbasierten Spezifikations- und Beweissysteme. Dazu gehört die Vorstellung eines Tableaukalküls für modale Logik und eine ausführliche Behandlung der sog. Charakterisierungstheorie, insbesondere im Hinblick auf ihren Zusammenhang mit der monadischen Logik zweiter Stufe.
- In diesem Kapitel wird ebenfalls auf Beschreibungslogiken und ihren Zusammenhang mit modaler Logik eingegangen,
- Einführung in die Dynamische Logik als Referenzmodell für Programmverifikationssysteme. Dazu gehört die Behandlung der dynamischen Aussagenlogik.
- Die im Stammmodul Formale Systeme [IN4INFS] eingeführte temporale Logik LTL wird um fortgeschritte Themen ergänzt und durch die Behandlung der temporalen Logik CTL ergänzt.
Lernziele
Der/Die Studierende soll
- das grundlegendene methodische Vorgehen der Theorie Formaler Systeme erlernen.
- anhand einiger ausgewählter Beispiele logische Theorien im Detail kennenlernen.
- einfache Aufgabenstellungen eigenständig bearbeiten und lösen können.
