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.

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

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)