Formale Systeme II: Theorie

Vorlesung im Sommersemester 2016

Prof. Dr. Bernhard Beckert (BB), Dr. Mattias Ulbrich (MU)

---

Zielgruppe:	Master Informatik
Veranst.-Nummer:	M-INFO-100841 / 24608
Umfang:	5 Leistungspunkte
Zeit:	Dienstags, 11:30 Uhr Freitags, 11:30 Uhr
Ort:	R236, Geb. 50.34

---

Aktuelles

• Am Dienstag, 07.06. findet keine Vorlesung statt.
• Am Freitag, 25.06. findet keine Vorlesung statt.
• Am Freitag, 8.7. findet keine Vorlesung statt.

---

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:

• Freitag, 22. April
• Freitag, 6. Mai (Brückentag)
• Freitag, 27. Mai (Brückentag)
• Dienstag, 7. Juni
• Freitag, 25. Juni
• Freitag, 8. Juli

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. Wir werden das Skript an einigen wenigen Stellen noch erweitern, also wird sich die Version dieses Dokuments gelegentlich ändern:

Skript (Version vom 23.08.2024, 22:38 Uhr)

Ergänzende Literatur

Dynamische Logic:

• D. Harel, D. Kozen, J. Tiury: Dynamic Logic (Foundations of Computing)
  MIT Press, 2000
  In der Fakultätsbibliothek vorhanden

Separation Logic

• John C. Reynolds: Separation Logic: A Logic for Shared Mutable Data Structures
  https://www.cs.cmu.edu/~jcr/seplogic.pdf
• Peter O'Hearn: A Primer on Separation Logic
  https://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/Marktoberdorf11LectureNotes.pdf
  Dias dazu

Termine

01.	VL am 19.04.	Organisatorisches Propositional Dynamic Logic (bis Dia 21, wird erweitert)
02.	VL am 26.04.	Propositional Dynamic Logic (bis Dia 43, wird erweitert)
03.	VL am 29.04.	Propositional Dynamic Logic (zu Ende) First Order Dynamic Logic (bis Dia 22, wird erweitert)
04.	VL am 03.05.	First Order Dynamic Logic (zu Ende) Übungsaufgaben
05.	VL am 10.05.	Logik in der Sozialwahltheorie: Teil A, Teil B, Teil C, Teil D Wesentliche Teile dieser Folien stammen von Ulle Endriss (Universität von Amsterdam)
06.	VL am 13.05.	Logik in der Sozialwahltheorie (Forsetzung)
07.	VL am 17.05.	Logik in der Sozialwahltheorie (Fortsetzung)
08.	VL am 20.05.	Differentielle Dynamische Logik Vorlesungsunterlagen von André Platzer an der CMU, insbesondere Lecture Notes.
09.	VL am 24.05.	Differentielle Dynamische Logik: Differentielle Invarianten Entscheidungsverfahren für semialgebraische Aussagen
10.	VL am 31.05.	Differentielle Dynamische Logik: Hybride Automaten, Übungen
11.	VL am 03.06.	Mehrwertige Logik
12.	VL am 10.06.	Mehrwertige Logik (Fortsetzung)
13.	VL am 14.06.	Mehrwertige Logik (Fortsetzung)
14.	VL am 17.06.	Separation Logic
15.	VL am 21.06.	Separation Logic (Fortsetzung)
16.	VL am 28.06.	Axiomatische Mengenlehre
17.	VL am 01.07.	Axiomatische Mengenlehre (Fortsetzung)
18.	VL am 05.07.	SAT und Phase Transition Die Folien stammen von Carsten Sinz, KIT
19.	VL am 12.07.	Implementierung von Beweissuche in Prolog: Folien Vergleich Suchstrategien Prolog-Programme dazu: search.pl, resolution.pl (zur Ausführung der Programme kann beispielsweise SWI Prolog verwendet werden)
20.	VL am 15.07.	Implementierung von Beweissuche in Prolog: Folien zum Tableaubeweiser leanTAP Prolog-Programme dazu: leantap.pl, leantest.pl, nnf.pl, unify.pl (zur Ausführung der Programme kann beispielsweise SWI Prolog verwendet werden)
21.	VL am 19.07.	Description Logic Die Folien stammen von Ulle Endriss (Universität von Amsterdam)

---

Prüfung

Mündlich nach Rücksprache mit den Dozierenden.