Formale Systeme II: Theorie
Vorlesung im Sommersemester 2018
Prof. Dr. Bernhard Beckert, Dr. Mattias Ulbrich
| Zielgruppe: | Master Informatik |
|---|---|
| Umfang: | 3 SWS / 5 Leistungspunkte |
| Vertiefungsfächer: | Theoretische Grundlagen |
| Ort: | SR 236 (Geb. 50.34) |
| Zeit: | Dienstag, 11:30 - 13:00 Uhr Freitag, 11:30 - 13:00 Uhr |
| Erstmals: | 24.04.2018 |
| Veranstaltungs-Nr.: | 24608 |
Termine
Die Vorlesung ist dreistündig, also wird an einigen Terminen im Verlauf des Semesters keine Veranstaltung stattfinden:
An folgenden Terminen findet keine Vorlesung statt:
- Dienstag, 17. April
- Freitag, 20. April
- Freitag, 11. Mai (Brückentag)
- Freitag, 18. Mai
- Freitag, 1. Juni (Brückentag)
- Dienstag, 10. Juli
- Freitag, 20. Juli
- ... Die Liste wird im Lauf des Semesters noch ergänzt werden.
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.
Skript
Das Skript von Prof. Peter H. Schmitt deckt viel des Stoffes dieser Vorlesung ab.
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
Vorlesungstermine und Materialien
| 1. | VL am 24.4. |
Organisatorisches Propositional Dynamic Logic (bis Dia 22, wird erweitert) |
| 2. | VL am 26.4. | Propositional Dynamic Logic (bis Dia 42, wird erweitert) |
| 3. | VL am 4.5. |
Propositional Dynamic Logic (zu Ende) First Order Dynamic Logic (bis Dia 22, wird erweitert) |
| 4. | VL am 8.5. |
First Order Dynamic Logic (zu Ende) Übungsaufgaben |
| 5. | VL am 15.5. | Logik in der Sozialwahltheorie:
Teil A,
Teil B,
Teil C,
Teil D Wesentliche Teile dieser Folien stammen von Ulle Endriss (Universität von Amsterdam) |
| 6. | VL am 22.5. | Logik in der Sozialwahltheorie (Forsetzung) |
| 7. | VL am 25.5. | Logik in der Sozialwahltheorie (Fortsetzung) |
| 8. | VL am 29.5. | Differentielle Dynamische Logik Vorlesungsunterlagen von André Platzer an der CMU, insbesondere Lecture Notes. |
| 9. | VL am 5.6. | Differentielle Dynamische Logik: Differentielle Invarianten |
| 10. | VL am 8.6. | Theorieschließen Ergänzend dazu: Gelungene Zusammenfassung der Quantoreneliminierung für Presburger Arithmetik. Neben dem Buch von Kroening und Strichman enthaelt auch Platzer's Buch etwas über Quantorenelimination, insbesondere für reelle Zahlen. |
| 11. | VL am 12.6. | Fortsetzung Theorieschließen (real closed fields, Kombination nach Nelson-Oppen) |
| 12. | VL am 15.6. | Mehrwertige Logik |
| 13. | VL am 19.6. | Mehrwertige Logik (Fortsetzung) |
| 14. | VL am 22.6. | SAT und Phasentransition |
| 15. | VL am 26.6. | Description Logic |
| 16. | VL am 29.6. | Prolog |
| 17. | VL am 3.7. | Prolog (Fortsetzung) |
| 18. | VL am 6.7. | Prolog (Demo) / Separation Logic (Einführung) Übersicht studentische Forschungsmöglichkeiten am Institut |
| 19. | VL am 13.7. | Separation Logic (Fortsetzung) |
| 20. | VL am 17.7. | Separation Logic (Fortsetzung) |