Formale Systeme II: Theorie
Vorlesung im Sommersemester 2022
Prof. Dr. Bernhard Beckert, Dr. Mattias Ulbrich
| Zielgruppe: | Master Informatik |
|---|---|
| Umfang: | 3 SWS / 5 Leistungspunkte, optional 5 Leistungspunkte (Forschungspraktikum, s.u.) |
| Vertiefungsfächer: | Theoretische Grundlagen |
| Ort: | SR 236 (Geb. 50.34) Es ist geplant, dass die Vorlesung mit Präsenzterminen stattfinden wird. |
| Zeit: | Dienstag, 11:30 - 13:00 Uhr Freitag, 11:30 - 13:00 Uhr |
| Erstmals: | 19.04.2022 |
| Veranstaltungs-Nr.: | 24608 |
| ILIAS-Kurs: | Link |
Bitte beachten Sie auch das Angebot, das vorlesungsbegleitende Forschungspraktikum (siehe unten) zu belegen.
Medien
Diese Vorlesung ist als Video-Playlist bei Youtube verfügbar.Skript
Das Skript von Prof. Peter H. Schmitt deckt viel des Stoffes dieser Vorlesung ab: Skript
Ergänzende Literatur
Dynamische Logic:
- D. Harel, D. Kozen, J. Tiury: Dynamic Logic (Foundations of Computing)
MIT Press, 2000
In der Fakultätsbibliothek vorhanden - André Platzer: Logical Analysis of Hybrid Systems
Springer, 2010
Online im KIT-Netz verfügbar - Daniel Kroening, Ofer Strichman: Decision Procedures
Springer, 2016, 2nd edition
Online im KIT-Netz verfügbar
Sozialwahltheorie:
- F. Brandt, V. Conitzer, U. Endriss, J. Lang, A. Procaccia (eds.):
Handbook of Computational Social Choice
Cambridge University Press, 2016
Download von Cambridge University Press
Folien und Materialien
- Organisatorisches
- Propositional Dynamic Logic
- First Order Dynamic Logic
- Axiomatische Mengenlehre
- Der erste Gödelsche Unvollständigkeitssatz
- Mehrwertige Logik (Teile 1 und 2)
- Logik in der Sozialwahltheorie
mit Folien 24-40 von Prof. Clemens Puppe (KIT) und Folien 48-85 von Prof. Ulle Endriss (Universität Amsterdam) - Theorien; Coopers Algorithmus
- Eine Einführung in Quantencomputing
- Differentielle Dynamische Logic für hybride Systeme – Logical Foundations of Cyber-Physical Systems
- Separation Logic
- Beschreibungslogiken (Description Logics)
Folien von Prof. Ulle Endriss (Universität Amsterdam)
Inhaltsübersicht
Geplant sind die folgenden Inhalte der Vorlesung:
- Grundlagen der modalen/dynamischen Logik
- Propositional Dynamic Logic (PDL)
- Vollständigkeit der PDL
- Relative Vollständigkeit der DL erster Stufe
- Tableaukalküle
- Separation Logic
- Deduktive Verifikation hybrider Modelle
- Axiomatische Mengenlehre nach Zermelo-Fraenkel
- Mehrwertige Logik
- Logik in der Sozialwahltheorie
- ...
Es kann noch zu kurzfristigen Änderungen des Curriculums kommen.
Termine
Die Vorlesung ist dreistündig, also wird an einigen Terminen im Verlauf des Semesters keine Veranstaltung stattfinden. Näheres wird hier (oder ggf. im Ilias-Kurs) bekannt gegeben.
An folgenden Terminen findet keine Vorlesung statt:
- Freitag, 29. April
- Freitag, 20. Mai
- Freitag, 27. Mai (Brückentag)
- Freitag, 03. Juni
- Dienstag, 07. Juni (Pfingstferien)
- Freitag, 10. Juni (Pfingstferien)
- Freitag, 17. Juni (Brückentag)
- Dienstag, 28. Juni
- Freitag, 1. Juli
- ... Die Liste wird im Lauf des Semesters noch ergänzt werden.
Vorlesungsbegleitendes Forschungspraktikum
Als Neuheit bieten wir neben der Vorlesung ein optionales begleitendes Forschungspraktikum im Umfang von insgesamt 5 LP (davon 2 SQ) an. Hierbei handelt es sich um ein Projektpraktikum, in dem über das ganze Semester an einem Thema gearbeitet wird (und nicht an verschiedenen Aufgabenblättern). Zu Beginn der Vorlesung werden Themen vorgestellt, für die sich die Teilnehmer:innen bewerben können. Das Forschungspraktikum basiert thematisch auf in der gekoppelten Vorlesung vermittelten Inhalten. Die praktische Forschungsaktivität ist Teil einer (größeren) Forschungsaktivität des Lehrstuhls und trägt zu deren Erfolg bei.
Beispiele für solche Forschungsaktivitäten sind etwa die Entwicklung eines Prototypen oder die Durchführung einer Evaluation (u.ä.). Am Ende des Semesters werden die Ergebnisse des Forschungspraktikums auf 3 bis 5 Seiten dokumentiert, sowie im Rahmen eines Kolloquiums in etwa 15 Minuten präsentiert und in einer anschließenden Fragerunde diskutiert.