Vorlesung Ausgewählte Kapitel der Logik: Lokalität
Aktuelles
- 2.7.26: neue, vollständige Version der Notizen zu Kapitel 5 hier bereitgestellt
- 30.6.26: neue Informationen zur Anmeldung zur Modulabschlussprüfung wurden hier bereitgestellt.
- 10.6.26: neue Informationen zur Zulassung zur Modulabschlussprüfung wurden hier bereitgestellt — in der Übungsstunde am 30.06.26 wird das Präsenzübungsblatt bearbeitet (dieses ist Teil der Voraussetzungen für die Zulassung zur Modulabschlussprüfung).
- 7.5.26: Am Dienstag, den 12.5.26 entfällt die Vorlesung, die Übung findet jedoch statt. Am Dienstag, den 19.5.26 findet die Vorlesung statt und an Stelle der Übung wird eine zusätzliche Vorlesung stattfinden.
- Die Eröffnungsvorlesung fand am Dienstag, den 14.04.26 ab 09:15 Uhr statt. Die erste Übungsstunde fand am Dienstag, den 21.04.26 statt.
- Im Logbuch finden Sie nach den Vorlesungen Informationen zum Inhalt der einzelnen Vorlesungsstunden und gelegentlich ergänzende Bemerkungen.
Einführung
Die mathematische Logik beschäftigt sich mit den grundlegenden Eigenschaften von formalen Systemen und Sprachen, insbesondere der Ausdrucksstärke von formalen Sprachen und Beweissystemen sowie den Möglichkeiten und Grenzen des automatischen Schließens. In dieser Vorlesung werden ausgewählte Kapitel der mathematischen Logik und deren Anwendungen in der Informatik im Kontext von Lokalitätsresultaten behandelt.
Themen der Vorlesung sind u. a. die Sätze von Gaifman und Hanf und die Anwendung von Lokalitätsresultaten zum Nachweis von Nicht-Ausdrückbarkeitsresultaten und zum Beweis von algorithmischen Meta-Theoremen.
Die Vorlesung richtet sich an fortgeschrittene Studierende in einem Masterstudiengang, die sich im Bereich der Logik spezialisieren wollen. Voraussetzung für die Teilnahme an der Veranstaltung sind Kenntnisse, die in der Vorlesung "Logik in der Informatik" vermittelt werden.
Inhalte
Das folgende Inhaltsverzeichnis wird im Laufe der Vorlesung noch ergänzt und möglicherweise verändert.
- Kapitel 0: Einleitung und Grundbegriffe (handschriftliche Notizen)
- Kapitel 1: Hanf-Normalform und Hanf-Lokalität (handschriftliche Notizen)
- Kapitel 2: Feferman-Vaught Zerlegungen (handschriftliche Notizen)
- Kapitel 3: Gaifman-Normalform und Gaifman-Lokalität (handschriftliche Notizen)
- Kapitel 4: Untere Schranken für die Größe von Formeln in Normalform (handschriftliche Notizen)
- Exkurs zum Thema Baumzerlegungen (handschriftliche Notizen)
- Kapitel 5: Model-Checking für FO und FO+MOD auf Klassen von beschränkter lokaler Baumweite (handschriftliche Notizen)
Beachten Sie: In den Vorlesungsstunden wird hauptsächlich an der Tafel gearbeitet. Alle behandelten Inhalte sind für die Veranstaltung wesentlich und daher auch dann prüfungsrelevant, wenn sie nicht in den auf den Webseiten erhältlichen Materialien enthalten sind.
Zur Vorbereitung auf eine Prüfung wird dringend empfohlen, das gesamte in den Vorlesungsstunden vermittelte Material durchzuarbeiten. Es ist daher wichtig, dass Sie sich während der Vorlesungs- und Übungsstunden Notizen machen.
Logbuch
Hier finden Sie nach den Vorlesungen Informationen zum Inhalt der einzelnen Vorlesungsstunden und gelegentlich ergänzende Bemerkungen.
Termine
- Vorlesung
- Dienstags 09:15-11:00 im ESZ (Rudower Chaussee 26), Raum 1.303 und
Donnerstags 11:15-13:00 im ESZ (Rudower Chaussee 26), Raum 1.303Dozentin: Prof. Dr. Nicole Schweikardt
- Übung
- Dienstags 11:00-13:00 im ESZ (Rudower Chaussee 26), Raum 1.303
Dozent: M.Sc. Johannes Friedrich Lange
Übungsblätter
Ab der zweiten Vorlesungswoche wird wöchentlich ein Übungsblatt ausgegeben und in der darauf folgenden Woche in der Übungsstunde besprochen. Auf jedem Übungsblatt können bis zu 100 Punkte erreicht werden.
- Blatt 1 (zu bearbeiten bis 28.04.)
- Blatt 2 (zu bearbeiten bis 05.05.)
- Blatt 3 (zu bearbeiten bis 12.05.)
- Blatt 4 (zu bearbeiten bis 26.05.)
- Blatt 5 (zu bearbeiten bis 02.06.)
- Blatt 6 (zu bearbeiten bis 09.06.)
- Blatt 7 (zu bearbeiten bis 16.06.)
- Blatt 8 (zu bearbeiten bis 23.06.)
- Blatt 9 (zu bearbeiten bis 07.07.)
- Blatt 10 (zu bearbeiten bis 14.07.)
Prüfung
Zur Vorbereitung auf eine Prüfung (Modulabschlussprüfung) ist es unbedingt notwendig, das gesamte in den Vorlesungs- und Übungsstunden vermittelte Material durchzuarbeiten.
Die Modulabschlussprüfung wird durch eine mündliche Prüfung abgelegt. Auf der Seite des Prüfungsbüros finden Sie den vollständigen Prüfungsplan (inkl. Prüfungszeitraum, Anmeldefristen).
Voraussetzung für die Zulassung zur Modulabschlussprüfung
- Erreichen von mindestens 50 Prozent aller Übungspunkte — um dies zu gewährleisten empfehlen wir dringend, regelmäßig und aktiv an den Übungsstunden teilzunehmen — und
- Erreichen von mindestens 40 Prozent der Punkte eines gesonderten Präsenzübungsblattes, welches in der Mitte des Semesters Übungsstunde am Dienstag, den 30.6.26 bearbeitet wird.
Verbindliche "Spielregeln" zum Erwerb von Übungspunkten
Übungsblätter werden dienstags nach der Vorlesung online zur Verfügung gestellt. Das jeweilige Übungsblatt wird in der Übungsstunde der darauf folgenden Woche besprochen. Sie können bei jedem Übungsblatt entscheiden, gemäß welcher der folgenden beiden Varianten A bzw. B Ihre Lösung bewertet werden soll:
- Variante A:
Sie geben eine handschriftliche, ausführlich ausgearbeitete und mathematisch präzise Lösung ab. Die Abgabe erfolgt bis spätestens Dienstag 09:00 Uhr durch Einwurf in den Briefkasten am Lehrstuhl (RUD25 zwischen den Räumen 3.401 und 3.402). - Variante B:
Sie geben keine Lösung ab. Stattdessen tragen Sie direkt vor Beginn der Übungsstunde in eine vom Übungsleiter bereitgestellte Liste ein, wie viele Übungspunkte Sie für Ihre Lösung der einzelnen Aufgaben(teile) für gerechtfertigt halten. Während der Übungsstunde werden vom Übungsleiter aus dieser Liste einzelne Teilnehmer:innen zum Vorrechnen von Aufgaben(teilen) ausgesucht. Falls sich beim Vorrechnen herausstellen sollte, dass Sie keine sinnvolle Lösung vorweisen können, obwohl Sie in der Liste Punkte für diese(n) Aufgabe(nteil) eingetragen haben, werden Ihnen für das gesamte gerade behandelte Übungsblatt keine Übungspunkte angerechnet. Eine sinnvolle Lösung muss hierbei nicht notwendigerweise vollständig korrekt sein.
Hinweise zur Prüfungsanmeldung
- Die Modulabschlussprüfung (kurz: MAP) wird als mündliche Prüfung durchgeführt. Dafür müssen Sie sich in AGNES anmelden – die Frist für die Anmeldung zum 1. Prüfungszeitraum endet am 2. Juli 2026! Beachten Sie, dass nur der Eintrag mit dem Zusatz "(mit Übungen)" in Agnes auf das richtige Modul verweist. Für jeden Prüfungstag gibt es eine separaten Eintrag. Melden Sie sich nur für einen der Tage an. Sie können sich auch anmelden, falls Sie die Voraussetzung zur Zulassung zur MAP zum jetzigen Zeitpunkt noch nicht erfüllen. Sollten Sie die Zulassung bis zum 18.7.26 nicht besitzen, werden Sie automatisch wieder abgemeldet (ohne dass dadurch Nachteile für Sie entstehen). Umgekehrt ist der 2. Juli 2026 eine harte Frist: Danach ist für den ersten Prüfungszeitraum keine Anmeldung mehr möglich!
- Zusätzlich zu der Anmeldung über Agnes benötigen Sie eine konkrete Prüfungszeit. Melden Sie sich dazu direkt nach Ihrer Anmeldung in Agnes per Mail an Silvia Schoch mit Prof. Nicole Schweikardt in cc. Nutzen Sie hierfür Ihre offizielle HU-Mail (CMS-Account) und geben Sie Ihren Namen, Ihre Matrikelnummer, das Modul (Ausgewählte Kapitel der Logik: Lokalität) und den in Agnes ausgewählten Prüfungstag an und bitten um die Zuteilung einer Prüfungszeit. Wichtig: zur Durchführung der MAP ist beides nötig: fristgerechte Anmeldung in Agnes und Vereinbarung einer konkreten Prüfungszeit.
Literatur
| [EFT] | H.-D. Ebbinghaus, J. Flum, W. Thomas, Einführung in die mathematische Logik, Springer Spektrum, 6. Auflage, 2018. |
| [S‑LI] | N. Schweikardt, Skript zur Vorlesung "Logik in der Informatik" im Wintersemester 2023/24, Humboldt-Universität zu Berlin. |
| [L] | Leonid Libkin, Elements of Finite Model Theory. Springer-Verlag, 2004. |
| [EF] | Heinz-Dieter Ebbinghaus und Jörg Flum, Finite Model Theory. Springer-Verlag, 2. Auflage, 1999. |
| [D] | Reinhard Diestel, Graph Theory. Springer-Verlag, 5. Auflage, 2017. Informationen zur deutschsprachigen Version finden sich hier. |
| [FG] | Jörg Flum und Martin Grohe, Parameterized Complexity. Springer-Verlag, 2006. |
| [FG01] | Markus Frick und Martin Grohe, Deciding First-Order Properties of Locally Tree-Decomposable Structures. In Journal of the ACM, Vol. 48, No. 6, November 2001, pp. 1184-1206. |
| [KS17] | Dietrich Kuske und Nicole Schweikardt, First-order logic with counting. In Proc. LICS 2017. Eine ausführlichere Vorabversion findet sich bei ArXiv unter der Nummer CoRR abs/1703.01122. |
| [BKS17] | Christoph Berkholz, Jens Keppeler und Nicole Schweikardt, Answering FO+MOD Queries Under Updates on Bounded Degree Databases. In Proc. ICDT 2017. Eine ausführlichere Vorabversion findet sich bei ArXiv unter der Nummer CoRR abs/1702.08764. |
| [KS18] | Dietrich Kuske und Nicole Schweikardt, Gaifman normal forms for counting extensions of first-order logic. In Proc. ICALP 2018. |
| [GS18] | Martin Grohe und Nicole Schweikardt, First-Order Query Evaluation with Cardinality Conditions. In Proc. PODS 2018, pp. 253-266. Eine ausführlichere Vorabversion findet sich bei ArXiv unter der Nummer CoRR abs/1707.05945. |
| [DGKS07] | Anuj Dawar, Stephan Kreutzer, Martin Grohe und Nicole Schweikardt, Model Theory Makes Formulas Large. In Proc. ICALP 2007, pp. 913-924. Eine ausführlichere Vorabversion findet sich hier. |
| [HKS13] | Lucas Heimberg, Dietrich Kuske und Nicole Schweikardt, An Optimal Gaifman Normal Form Construction for Structures of Bounded Degree. In Proc. LICS 2013, pp. 63-72. |
| [HKS16] | Lucas Heimberg, Dietrich Kuske und Nicole Schweikardt, Hanf normal form for first-order logic with unary counting quantifiers. In Proc. LICS 2016, pp. 277-286. |
Zugang zur Online-Literatur
Einige der Bücher sind für Angehörige der HU Berlin online erhältlich (siehe Verlinkung). Loggen Sie sich dazu auf der Springerlink-Seite via Shibboleth mit ihrem CMS-Account ein (über Log In, Access via your institution bzw. Shibboleth-Login, Find your institution: Humboldt-Universität zu Berlin). Alternativ können Sie ggf. über eine VPN-Verbindung über das HU-Netz direkt darauf zugreifen. Zur Einrichtung eines VPN-Zugangs siehe die Anleitung des CMS.
Links
| [LICS] | IEEE Symposium on Logic in Computer Science (LICS) |
| [EACSL] | European Association for Computer Science Logic (EACSL) |
| [Highlights] | Highlights in Logic, Games and Automata |