Seminar Logik, Komplexität, Spiele: Endliche Modelltheorie

WS 2012/13

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:0009:45Norman MüllerLokalität der Prädikatenlogik: Die Sätze von Hanf und Gaifman
09:4510:30Martin RitzertZusammenhänge und Charakterisierungen verschiedener Lokalitätskonzepte
10:4511:30Evgeny SaleevEine logische Charakterisierung von Lokalität
11:3012:15Felix CanavoiMonadisches NP vs. monadisches co-NP
13:3014:15Daniel NeuenErweiterungen von monadischem NP
14:1515:00Martin BellgardtEndliche Modelltheorie erzeugt lange Formeln
Mittwoch, 30. Januar
08:3009:15Marlene GregorekKlassische Werkzeuge der Modelltheorie angewandt im Endlichen
09:1510:00Patrick LandwehrÄquivalenz in der k-Variablen Logik ist vollständig für PTIME
10:1511:00Waldemar LaubeAlgorithmische Komplexität von Ehrenfeucht-Fraïsse Spielen
11:0011:45Svenja SchalthöferUnterscheidbarkeit von Strukturen in existentieller k-Variablen Logik
13:3014:15Wadim PessinLineare Gleichungssysteme und Äquivalenz in der k-Variablen Logik
14:1515:00Stefan BleßLokalität von ordnungs-invarianter Prädikatenlogik
15:1516:00Matthias KlupschAusdrucksstä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

ThemaVortragende(r)Betreuer(in)Literatur
Lokalität der Prädikatenlogik: Die Sätze von Hanf und GaifmanNorman MüllerSimon Lessenich[Li04, EbFl95]
Zusammenhänge und Charakterisierungen verschiedener LokalitätskonzepteMartin RitzertSimon Lessenich[HeLiNu99, Li04]
Eine logische Charakterisierung von LokalitätEvgeny SaleevFaried Abu Zaid[Li01]
Monadisches NP vs. monadisches co-NPFelix CanavoiWied Pakusa[FaStVa95]
Erweiterungen von monadischem NPDaniel NeuenWied Pakusa[AjFaSt00, JaMa01]
Endliche Modelltheorie erzeugt lange FormelnMartin BellgardtFaried Abu Zaid[DaGrKrSc07]
Klassische Werkzeuge der Modelltheorie angewandt im EndlichenMarlene GregorekRoman Rabinovich[LiWe12]
Äquivalenz in der k-Variablen Logik ist vollständig für PTIMEPatrick LandwehrBernd Puchala[Gr99]
Algorithmische Komplexität von Ehrenfeucht-Fraïsse SpielenWaldemar LaubeBernd Puchala[Pe98]
Unterscheidbarkeit von Strukturen in existentieller k-Variablen LogikSvenja SchalthöferBernd Puchala[KoPa03, Be12]
Lineare Gleichungssysteme und Äquivalenz in der k-Variablen LogikWadim PessinWied Pakusa[GrOt12]
Lokalität von ordnungs-invarianter PrädikatenlogikStefan BleßDiana Fischer[GrSc00]
Ausdrucksstärke von Prädikatenlogik mit invarianten OperatorenMatthias KlupschDiana 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