Algorithmische Modelltheorie
WS 2013/14
Aktuelles
- Ab sofort startet die Übung um 16:15h.
- Übungsbetrieb: Die Übungen können in Gruppen bearbeitet werden (max. 3 Studenten) und sind spätestens Montags um 12 Uhr im Kasten am Lehrstuhl (bzw. zuvor in der Vorlesung) abzugeben. Neue Aufgabenblätter werden in der Regel Montags auf der Homepage verfügbar sein.
Termine
| Art | Termin | Ort | Veranstalter | ||||
|---|---|---|---|---|---|---|---|
| V4 | Mo 10:15 – 11:45 | AH II | Beginn 21. Oktober | E. Grädel | |||
| Mi 12:15 – 13:45 | AH II | Beginn 16. Oktober | E. Grädel | ||||
| Ü2 | Mi 16:15 – 17:45 | AH I | Beginn 30. Oktober | F. Abu Zaid, W. Pakusa, F. Reinhardt | |||
Übungen
- Übung 1 [pdf]
- Übung 2 [pdf]
- Übung 3 [pdf]
- Übung 4 [pdf]
- Übung 5 [pdf]
- Übung 6 [pdf]
- Übung 7 [pdf]
- Übung 8 [pdf]
- Übung 9 [pdf]
- Übung 10 [pdf]
- Übung 11 [pdf]
- Übung 12 [pdf]
Skript
Skript
- Kapitel 1: The Classical Decision Problem for FO [pdf] [pdf-2up]
- Kapitel 2: Finite Model Property [pdf] [pdf-2up]
- Kapitel 3: Descriptive Complexity [pdf] [pdf-2up]
- Kapitel 4: LFP and Infinitary Logics [pdf] [pdf-2up]
- Kapitel 5: Modal, Inflationary and Partial Fixed Points [pdf] [pdf-2up]
- Kapitel 6: Fixed-point logic with counting [pdf] [pdf-2up]
- Kapitel 7: Zero-one laws [pdf] [pdf-2up]
Inhalt
- Entscheidbare und unentscheidbare Theorien
- Endliche-Modell-Eigenschaft
- Deskriptive Komplexität: Logische Charakterisierung von Komplexitätsklassen
- Lokalität der Prädikatenlogik, 0-1-Gesetze
- Logiken mit transitiver Hülle, Fixpunktlogiken
Lernziele
- Verständnis der Zusammenhänge von logischer Definierbarkeit und algorithmischer Komplexität (Entscheidbarkeit von Theorien, Auswertungsalgorithmen, logische Charakterisierungen von Komplexitätsklassen).
- Beherrschen der modelltheoretischen und algorithmischen Methoden zur Analyse der Ausdrucksstärke und Komplexität logischer Spezifikationen auf endlichen und endlich präsentierbaren Strukturen.
- Fähigkeit, mit den fundamentalen Logiken der algorithmischen Modelltheorie umzugehen und diese in konkreten Szenarien anzuwenden.
Literatur
| [1] | S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison-Wesley, 1995. |
| [2] | E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Springer-Verlag, 1997. |
| [3] | H. Ebbinghaus and J. Flum. Finite Model Theory. Springer, 1999. |
| [4] | 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. |
| [5] | E. Grädel. Finite Model Theory and Descriptive Complexity. In Finite Model Theory and Its Applications, pp. 125–230. Springer-Verlag, 2007. |
| [6] | N. Immerman. Descriptive Complexity. Springer, 1999. |
| [7] | L. Libkin. Elements of Finite Model Theory. Springer, 2004. |
Voraussetzungen
- Mathematische Logik
Zuordnung
- Computermathematik (D)/Hauptstudium/Hauptfach Computermathematik
- Informatik (D)/Hauptstudium/Theoretische Informatik
- Informatik (D)/Anwendungsfächer/Mathematik
- Mathematik (D)/Hauptstudium/Reine Mathematik
- Informatik (M.A.)/Hauptstudium
- Mathematik (M.A.)
- Technik-Kommunikation (M.A.)/2. Hauptfach (Technisches Fach)/Grundlagen der Informatik/Hauptstudium/Spezialisierung Informatik
- Informatik (GYM+GS,SII)/Hauptstudium/C. Mathematische Methoden der Informatik
- Mathematik (B.Sc.)/Mathematik (WS)/5. Semester
- Mathematik (B.Sc.)/Mathematik (SS)/6. Semester
- Informatik (M.Sc.)/Theoretische Informatik
- Mathematik (M.Sc.)/Mathematik/Reine Mathematik
- Software Systems Engineering (M.Sc.)/Theoretical Foundations of Software Systems Engineering
- Software Systems Engineering (M.Sc.)/[MPO2010] Theoretical Computer Science
Leistungsnachweis
- Bachelor- und Masterstudiengänge: Lösen von 50% der Übungsaufgaben und Bestehen einer mündlichen Prüfung im Umfang von 30 Minuten
- Diplomstudiengänge: Übungsschein bei Lösen von 50% der Übungsaufgaben und aktiver Teilnahme an den Übungen
Rückfragen
Erich Grädel, Wied Pakusa, Faried Abu Zaid