Aktuelles

• Die Seminarvorträge finden am 17. Juli statt.
• Die Themen- und Betreuer-Zuteilung sowie ein vorläufiger Zeitplan stehen fest.
• Als einführende Lektüre zum Thema Fixpunktlogiken und deskriptive Komplexität empfehlen wir Kapitel 3 aus Finite Model Theory and Its Applications [GKL+07].

Programm

Freitag, 17. Juli
10:00	–	10:45	Malte Nuhn	Der modale μ-Kalkül
10:45	–	11:30	Vladislavs Serebro	Inflationäre Fixpunkte in der Modallogik
11:30	–	11:45		Kaffeepause
11:45	–	12:30	Florian Weingarten	Fixpunktlogik mit Zählquantoren
12:30	–	13:30		Mittagspause
13:30	–	14:15	Jonathan Höges	Bisimulations-invariantes PTime und höherdimensionaler mu-Kalkül

Organisation

Die Veranstaltung wird als Blockseminar am Ende der Vorlesungszeit durchgeführt. Die Vorbesprechung findet am Donnerstag, den 19. März um 10 Uhr in Raum 4116 (Seminarraum des Lehrstuhls) statt.

Zeitplan

06.04.	Gliederung
04.05.	Ausarbeitung
29.05.	Endgültige Fassung
15.06.	Folien

Inhalt

Fixpunktkalküle spielen in der Mathematischen Logik und in vielen Bereichen der Informatik eine zentrale Rolle. Wichtige Beispiele sind:

• Fixpunktlogiken wie LFP, IFP, PFP als Erweiterung der Prädikatenlogik, mit Anwendungen in der deskriptiven Komplexitätstheorie.
• Der modale μ-Kalkül (und dessen Fragmente, wie etwa PDL oder die temporalen Logiken LTL, CTL, CTL*) mit wichtigen Anwendungen in der automatischen Verifikation (via Model-Checking).
• Die Datenbank-Anfragesprache Datalog und deren Erweiterungen zur Formalisierung von Anfragen, welche Rekursion bzw. unbeschränkte Iteration erfordern und daher in einfachen Formalismen wie der relationalen Algebra oder SQL nicht ausgedrückt werden können.
• Modale Logiken in der Wissensrepräsentation, mit Fixpunkten etwa zur Beschreibung von "common knowledge".

Im Seminar werden, ausgehend von den Grundlagen von Fixpunkt-Konstrukten, algorithmische, komplexitätstheoretische und modelltheoretische Fragen behandelt.

Themen

Thema	Vortragende(r)	Betreuer(in)	Literatur
Der modale μ-Kalkül	Malte Nuhn	M. Ummels	[Kir02, Zap02]
Das stetige Fragment des μ-Kalküls	Julian Pott	D. Fischer	[Fon08]
Äquivalenz von LFP und IFP	Lars Feyerabend	Ł. Kaiser	[Kre02a, Kre02b, GS86]
Inflationäre Fixpunkte in der Modallogik	Vladislavs Serebro	M. Ummels	[DGK04, Kre02b]
Fixpunktlogik mit Zählquantoren	Florian Weingarten	R. Rabinovich	[FG00]
Bisimulations-invariantes PTime und höherdimensionaler mu-Kalkül	Jonathan Höges	B. Puchala	[Ott99, GKL+07]
Der Satz von Abiteboul und Vianu	André Goliath	T. Ganzow	[Daw93, DLW95, Ott08]

Literatur

[DGK04]	A. Dawar, E. Grädel, and S. Kreutzer. Inflationary fixed points in modal logic. ACM Transations on Computational Logic, vol. 5, pp. 282–315, 2004.
[DLW95]	A. Dawar, S. Lindell, and S. Weinstein. Infinitary Logic and Inductive Definability over Finite Structures. Information and Computation, vol. 119, pp. 160–175, 1995.
[Dah87]	E. Dahlhaus. Skolem Normal Forms Concerning the Least Fixpoint. In Computation Theory and Logic (E. Börger, Ed.), vol. 270 of LNCS, pp. 101–106. Springer, 1987.
[Daw93]	A. Dawar. Feasible Computation through Model Theory. PhD thesis, University of Pennsylvania, 1993.
[EF95]	H. Ebbinghaus and J. Flum. Finite Model Theory. Springer-Verlag, 1995.
[FG00]	J. Flum and M. Grohe. On fixed-point logic with counting. J. Symbolic Logic, vol. 65-2, pp. 777–787, 2000.
[Fon08]	G. Fontaine. Continuous Fragment of the mu-Calculus. In Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings (M. Kaminski and S. Martini, Eds.), vol. 5213 of Lecture Notes in Computer Science, pp. 139–153. Springer, 2008.
[GKL+07]	E. Grädel, P. G. Kolaitis, L. Libkin, M. Marx, J. Spencer, M. Y. Vardi, Y. Venema, and S.Weinstein. Finite Model Theory and Its Applications. Springer-Verlag, 2007.
[GS86]	Y. Gurevich and S. Shelah. Fixed-Point extensions of first order logic. Annals of Pure and Applied Logic, vol. 32, pp. 265–280, 1986.
[Kir02]	D. Kirsten. Alternating Tree Automata and Parity Games. In Automata, Logics, and Infinite Games (E. Grädel, W. Thomas, and T. Wilke, Eds.), vol. 2500 of Lecture Notes in Computer Science, pp. 153–167. Springer-Verlag, 2002.
[Kre02a]	S. Kreutzer. Expressive Equivalence of Least and Inflationary Fixed-Point Logic. In Proceedings of the 17th IEEE Symp. on Logic in Computer Science (LICS), 2002.
[Kre02b]	S. Kreutzer. Pure and Applied Fixed-Point Logics. PhD thesis, RWTH Aachen, 2002.
[Ott08]	M. Otto. Finite Model Theory. 2008.
[Ott98b]	M. Otto. Bisimulation-Invariant Ptime and Higher-Dimensional mu-Calculus. Theoretical Computer Science, vol. 224, pp. 237–265, 1999.
[Zap02]	J. Zappe. Modal $\mu$-Calculus and Alternating Tree Automata. In Automata, Logics, and Infinite Games (E. Grädel, W. Thomas, and T. Wilke, Eds.), vol. 2500 of Lecture Notes in Computer Science, pp. 171–184. Springer-Verlag, 2002.

Zuordnung

• Mathematik-Studiengänge: Diplom, Bachelor, Lehramt (SII), Computermathematik
• Informatik-Studiengänge: Diplom, Bachelor, Lehramt (SII)

Voraussetzungen

• Übungsschein Mathematische Logik
• für B.Sc. Informatik: bestandenes Modul "Einführung in das wissenschaftliche Arbeiten (Proseminar)"

Rückfragen

Erich Grädel, Diana Fischer, Tobias Ganzow, Łukasz Kaiser, Bernd Puchala, Roman Rabinovich, Michael Ummels