Aktuelles

Die Vorträge finden statt am:

• Dienstag, 29. Januar, im Seminarraum des Lehrstuhls i2 (Raum 4201b, E1, Ahornstr. 55)
• Mittwoch, 30. Januar, in unserem Seminarraum (Raum 4116, E1, Ahornstr. 55)

Die Vorträge können wahlweise auf deutsch oder englisch gehalten werden.

Organisation

Die Veranstaltung wird als Blockseminar angeboten.

Zeitplan

22.10.	Gliederung, Konzeption
19.11.	Ausarbeitung
10.12.	Endgültige Fassung
14.01.	Folien
29.01., 30.01.	Vorträge

Programm

Dienstag, 29. Januar
09:00	–	09:45	Norman Müller	Lokalität der Prädikatenlogik: Die Sätze von Hanf und Gaifman
09:45	–	10:30	Martin Ritzert	Zusammenhänge und Charakterisierungen verschiedener Lokalitätskonzepte
10:45	–	11:30	Evgeny Saleev	Eine logische Charakterisierung von Lokalität
11:30	–	12:15	Felix Canavoi	Monadisches NP vs. monadisches co-NP
13:30	–	14:15	Daniel Neuen	Erweiterungen von monadischem NP
14:15	–	15:00	Martin Bellgardt	Endliche Modelltheorie erzeugt lange Formeln
Mittwoch, 30. Januar
08:30	–	09:15	Marlene Gregorek	Klassische Werkzeuge der Modelltheorie angewandt im Endlichen
09:15	–	10:00	Patrick Landwehr	Äquivalenz in der k-Variablen Logik ist vollständig für PTIME
10:15	–	11:00	Waldemar Laube	Algorithmische Komplexität von Ehrenfeucht-Fraïsse Spielen
11:00	–	11:45	Svenja Schalthöfer	Unterscheidbarkeit von Strukturen in existentieller k-Variablen Logik
13:30	–	14:15	Wadim Pessin	Lineare Gleichungssysteme und Äquivalenz in der k-Variablen Logik
14:15	–	15:00	Stefan Bleß	Lokalität von ordnungs-invarianter Prädikatenlogik
15:15	–	16:00	Matthias Klupsch	Ausdrucksstärke von Prädikatenlogik mit invarianten Operatoren

Inhalt

In diesem Seminar sollen grundlegende Konzepte und Methoden der Endlichen Modelltheorie und einige ihrer Anwendungen vorgestellt werden.

Die Endliche Modelltheorie untersucht die Eigenschaften und das Verhalten von Logiken (wie z.B. der Prädikatenlogik) die sich ergeben, wenn als mögliche Modelle nur endliche Strukturen betrachtet werden. Klassische Fragestellungen umfassen etwa die relative Ausdrucksstärke verschiedener Logiken untereinander, oder die strukturelle und algorithmische Komplexität von definerbaren Strukturklassen sowie deren asymptotische Wahrscheinlichkeit. Hierbei sind Zusammenhänge zwischen logischer Definierbarkeit und algorithmischer Komplexität von Klassen endlicher Strukturen von besonderem Interesse.

Es stellt sich heraus, dass viele Werkzeuge der klassischen Modelltheorie, wie etwa der Kompaktheitssatz oder der Vollständigkeitssatz für die Prädikatenlogik, auf der Klasse der endlichen Strukturen nicht zur Verfügung stehen. Allerdings bleibt die Charakterisierung der Ausdrucksstärke von FO durch Ehrenfeucht-Fraïsse Spiele auch im Endlichen erhalten.

Aus diesem Grund nehmen in der Endlichen Modelltheorie kombinatorische und spieltheoretische Argumente eine zentrale Rolle ein. So kann mit Hilfe von Ehrenfeucht-Fraïsse Spielen etwa gezeigt werden, dass alle in FO definierbaren Relationen (in einem präzisen Sinne) lokal sind (z.B. Erreichbarkeit in Graphen kann nicht ausgedrückt werden), oder dass ein Satz der Prädikatenlogik entweder in fast allen oder fast keiner endlichen Struktur gilt.

Folgenden Aspekte werden innerhalb des Seminars genauer thematisiert:

• Ehrenfeucht-Fraïsse Spiele;
• Lokalitätsbegriffe für (Erweiterungen von) FO;
• Model-Checking Probleme für FO;
• k-Variablen Fragmente von FO;
• Logische Operatoren für Erreichbarkeit;
• 0-1 Gesetze.

Für das Seminar sind Kenntnisse aus der Vorlesung Mathematische Logik notwendig; Kenntnisse aus der Vorlesung Algorithmische Modelltheorie sind wünschenswert, aber nicht notwendig.

Themen

Thema	Vortragende(r)	Betreuer(in)	Literatur
Lokalität der Prädikatenlogik: Die Sätze von Hanf und Gaifman	Norman Müller	Simon Lessenich	[Li04, EbFl95]
Zusammenhänge und Charakterisierungen verschiedener Lokalitätskonzepte	Martin Ritzert	Simon Lessenich	[HeLiNu99, Li04]
Eine logische Charakterisierung von Lokalität	Evgeny Saleev	Faried Abu Zaid	[Li01]
Monadisches NP vs. monadisches co-NP	Felix Canavoi	Wied Pakusa	[FaStVa95]
Erweiterungen von monadischem NP	Daniel Neuen	Wied Pakusa	[AjFaSt00, JaMa01]
Endliche Modelltheorie erzeugt lange Formeln	Martin Bellgardt	Faried Abu Zaid	[DaGrKrSc07]
Klassische Werkzeuge der Modelltheorie angewandt im Endlichen	Marlene Gregorek	Roman Rabinovich	[LiWe12]
Äquivalenz in der k-Variablen Logik ist vollständig für PTIME	Patrick Landwehr	Bernd Puchala	[Gr99]
Algorithmische Komplexität von Ehrenfeucht-Fraïsse Spielen	Waldemar Laube	Bernd Puchala	[Pe98]
Unterscheidbarkeit von Strukturen in existentieller k-Variablen Logik	Svenja Schalthöfer	Bernd Puchala	[KoPa03, Be12]
Lineare Gleichungssysteme und Äquivalenz in der k-Variablen Logik	Wadim Pessin	Wied Pakusa	[GrOt12]
Lokalität von ordnungs-invarianter Prädikatenlogik	Stefan Bleß	Diana Fischer	[GrSc00]
Ausdrucksstärke von Prädikatenlogik mit invarianten Operatoren	Matthias Klupsch	Diana Fischer	[Ot00, Ro07]

Literatur

[AHV95]	S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison-Wesley, 1995.
[AjFaSt00]	M. Ajtai, R. Fagin, and L. J. Stockmeyer. The Closure of Monadic NP. J. Comput. Syst. Sci., vol. 60(3), pp. 660-716, 2000.
[Be12]	C. Berkholz. Lower Bounds for Existential Pebble Games and k-Consistency Tests. CoRR, vol. abs/1205.0679, 2012.
[BoGrGu97]	E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Springer-Verlag, 1997.
[DaGrKrSc07]	A. Dawar, M. Grohe, S. Kreutzer, and N. Schweikardt. Model Theory Makes Formulas Large. In ICALP, pp. 913-924, 2007.
[DuGr07]	A. Durand and E. Grandjean. First-order queries on structures of bounded degree are computable with constant delay. ACM Trans. Comput. Log., vol. 8(4), 2007.
[EF99]	H. Ebbinghaus and J. Flum. Finite Model Theory. Springer, 1999.
[EbFl95]	H. Ebbinghaus and J. Flum. Finite model theory. Springer, 1995.
[FMT07]	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.
[FaStVa95]	R. Fagin, L. J. Stockmeyer, and M. Y. Vardi. On Monadic NP vs. Monadic co-NP. Inf. Comput., vol. 120(1), pp. 78-92, 1995.
[FrGr01]	M. Frick and M. Grohe. Deciding first-order properties of locally tree-decomposable structures. J. ACM, vol. 48(6), pp. 1184-1206, 2001.
[Gr99]	M. Grohe. Equivalence in Finite-Variable Logics is Complete for Polynomial Time. Combinatorica, vol. 19(4), pp. 507-532, 1999.
[GrOt12]	M. Grohe and M. Otto. Pebble Games and Linear Equations. CoRR, vol. abs/1204.1990, 2012.
[GrSc00]	M. Grohe and T. Schwentick. Locality of order-invariant first-order formulas. ACM Trans. Comput. Log., vol. 1(1), pp. 112-130, 2000.
[Graedel07]	E. Grädel. Finite Model Theory and Descriptive Complexity. In Finite Model Theory and Its Applications, pp. 125–230. Springer-Verlag, 2007.
[HeLiNu99]	L. Hella, L. Libkin, and J. Nurmonen. Notions of Locality and Their Logical Characterizations over Finite Models. J. Symb. Log., vol. 64(4), pp. 1751-1773, 1999.
[Hod93]	W. Hodges. Model theory. Cambridge University Press, 1993.
[Imm99]	N. Immerman. Descriptive Complexity. Springer, 1999.
[JaMa01]	D. Janin and J. Marcinkowski. A Toolkit for First Order Extensions of Monadic Games. In STACS, pp. 353-364, 2001.
[KaSe11]	W. Kazana and L. Segoufin. First-order query evaluation on structures of bounded degree. Logical Methods in Computer Science, vol. 7(2), 2011.
[KoPa03]	P. G. Kolaitis and J. Panttaja. On the Complexity of Existential Pebble Games. In CSL, pp. 314-329, 2003.
[Li01]	L. Libkin. Logics capturing local properties. ACM Trans. Comput. Log., vol. 2(1), pp. 135-153, 2001.
[Li04]	L. Libkin. Elements of Finite Model Theory. Springer, 2004.
[LiWe12]	S. Lindell and S. Weinstein. Infinitary methods in finite model theory. To appear, 2012.
[Lib04]	L. Libkin. Elements of Finite Model Theory. Springer, 2004.
[Ot00]	M. Otto. Epsilon-Logic Is More Expressive Than First-Order Logic Over Finite Structures. J. Symb. Log., vol. 65(4), pp. 1749-1757, 2000.
[Pe98]	E. Pezzoli. Computational Complexity of Ehrenfeucht-Fra\"\issé Games on Finite Structures. In CSL, pp. 159-170, 1998.
[Ro07]	B. Rossman. Successor-invariant first-order logic on finite structures. J. Symb. Log., vol. 72(2), pp. 601-618, 2007.
[Se96]	D. Seese. Linear Time Computable Problems and First-Order Descriptions. Mathematical Structures in Computer Science, vol. 6(6), pp. 505-526, 1996.
[csl1998]	G. Gottlob, E. Grandjean, and K. Seyr (Eds.). Computer Science Logic, 12th International Workshop, CSL '98, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998, Proceedings. Springer, 1999.
[csl2003]	M. Baaz and J. A. Makowsky (Eds.). Computer Science Logic, 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt Gödel Colloquium, KGC 2003, Vienna, Austria, August 25-30, 2003, Proceedings. Springer, 2003.
[icalp2007]	L. Arge, C. Cachin, T. Jurdzinski, and A. Tarlecki (Eds.). Automata, Languages and Programming, 34th International Colloquium, ICALP 2007, Wroclaw, Poland, July 9-13, 2007, Proceedings. Springer, 2007.
[stacs2001]	A. Ferreira and H. Reichel (Eds.). STACS 2001, 18th Annual Symposium on Theoretical Aspects of Computer Science, Dresden, Germany, February 15-17, 2001, Proceedings. Springer, 2001.

Zuordnung

• Informatik (B.Sc.)/Seminar Informatik
• Mathematik (B.Sc.)/Seminar: Logik, Komplexität, Spiele
• Informatik (M.Sc.)/Seminar Theoretische Informatik
• Mathematik (M.Sc.)/Seminar: Logik, Komplexität, Spiele (Reine Mathematik)
• Informatik (D)/Hauptstudium/Theoretische Informatik
• Mathematik (D)/Hauptstudium/Reine Mathematik
• Informatik (S II)
• Mathematik (S II)/Hauptstudium/Modul Algebra
• Mathematik (S II)/Hauptstudium/Modul Angewandte Mathematik

Voraussetzungen

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

Rückfragen

Erich Grädel, Faried Abu Zaid, Diana Fischer, Simon Lessenich, Wied Pakusa, Bernd Puchala, Roman Rabinovich