|
Logik in der Informatik
Prof. Dr. Nicole Schweikardt |
|
Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden und gelegentlich auch Korrekturen und sonstige ergänzende Bemerkungen.
Kapitel 0: Einleitung und Grundbegriffe — heute: Einführung ins Thema, Organisatorisches, Vereinbarungen und Notationen bzgl. logischen Strukturen, Signaturen etc.; Definition von Syntax und Semantik der Logik FO+MOD; Beispiele
Material:
handschriftliche Notizen zu Kapitel 0: heute Seiten 0.1–0.4
Weitere Lektüre:
[KS17]
Kapitel 0: Einleitung und Grundbegriffe — heute: Einführung des Begriffs "Zählterm"; Syntax und Semantik der Logik FO(P) (eine Erweiterung der Logik erster Stufe um unäre Zählquantoren); Beispiele; Syntax und Semantik der Logik FOC(P) (eine Erweiterung der Logik erster Stufe um Zählterme und numerische Prädikate); Beispiele; weitere Grundbegriffe: der Gaifman-Graph, der Grad und die Zusammenhangskomponenten einer Struktur, die Distanz zwischen Elementen im Universum einer Struktur, induzierte Substrukturen, Nachbarschaften, r-Typen mit k Zentren über einer Signatur σ (und Beispiele dazu)
Material:
handschriftliche Notizen zu Kapitel 0: heute Seiten 0.5–0.11
Weitere Lektüre:
[KS17]
Abschluss von Kapitel 0: Einleitung und Grundbegriffe — heute: r-Typen mit k Zentren über einer Signatur σ und deren Beschreibung durch FO[σ]-Sätze; eine obere Schranke für die Anzahl der Elemente in der r-Nachbarschaft eines Elements im Universum einer Struktur vom Grad höchstens d; weitere einfache Beobachtungen zu Typen und Nachbarschaften; Korrektur: Bei Lemma 0.3(c) gilt nur die Richtung von links nach rechts; für die Richtung von rechts nach links haben wir ein Gegenbeispiel behandelt [Quelle: Charlotte Lenz, Masterarbeit, 2025, Seiten 5-6] und eine zusätzliche Voraussetzung formuliert, unter der auch die Richtunng von rechts nach links korrekt ist.
Material:
handschriftliche Notizen zu Kapitel 0: heute Seiten 0.8–0.16
Weitere Lektüre:
[KS17]
Start mit Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: Definition der Begriffe Typen-1-Zählterm, einfacher-Zählterm, Hanf-Zählsatz und HNF-Formel für FO(P); Formulierung des Theorems zur "schwachen Hanf-Normalform für FO(P)" (Theorem 1.5); Diskussion zu Anwendungsmöglichkeiten des Theorems: Linearzeit-Auswertung von FO(P)-Sätzen auf Strukturen vom Grad höchstens d; Formulierung und Beginn des Beweises des ersten technischen Lemmas, das für den Beweis von Theorem 1.5 gebraucht wird (Lemma 1.6)
Material:
handschriftliche Notizen zu Kapitel 1: heute Seiten 1.1–1.7
Weitere Lektüre:
[KS17]
Weiter mit Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: Abschluss des Beweise von Lemma 1.6; Formulierung und Beweis von Lema 1.7; Beginn des Beweises von Theorem 1.5
Material:
handschriftliche Notizen zu Kapitel 1: heute Seiten 1.8–1.17
Weitere Lektüre:
[KS17]
Weiter mit Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: Abschluss des Beweises von Theorem 1.5; direkte Folgerungen aus dem Beweis (Radius der HNF-Formel und Laufzeit zur Konstruktion der Formel); Anwendungen von Theorem 1.5: Hanf-Normalform für die Logik FO
Material:
handschriftliche Notizen zu Kapitel 1: heute
Seiten 1.17–1.24
Weitere Lektüre:
[KS17]
Weiter mit Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: weitere Anwendungen von Theorem 1.5: Hanf-Normalform für die Logik FO+MOD; die Hanf-Lokalität von FO(P) und ihre Verwendung zum Nachweis von Nicht-Ausdrückbarkeit in FO(P)
Material: handschriftliche Notizen zu Kapitel 1:
heute Seiten 1.25–1.32
Weitere Lektüre:
[KS17]
(vorerst) Abschluss von Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute:
Anwendungen von Theorem 1.5: algorithmische Meta-Theoreme: ein Linearzeit-Algorithmus für EVALφ,d für einen beliebigen FO(P)-Satz φ und eine Gradschranke d (Verallgemeinerung des Satzes von Seese);
Einführung des Zähl-Problems COUNTφ(x1,...,xn),d und des Aufzählungs-Problems
ENUMφ(x1,...,xn),d für eine FO(P)-Formel φ mit freien Variablen aus x1,...,xn und eine Gradschranke d; Ausblick auf ein Resultat (heute ohne Beweis), das besagt, dass das Zähl-Problem in Linearzeit und das Aufzählungs-Problem mit konstanter Taktung nach Linearzeit-Vorverarbeitung gelöst werden kann
Start mit Kapitel 2: Feferman-Vaught-Zerlegungen — heute:
Definition des Begriffs einer Feferman-Vaught-Zerlegung einer Formel φ bzgl. (x;y) (für Variablentupel x und y); ein Beispiel; Ausblick auf die Aussage, die wir in diesem Kapitel beweisen wollen
Material:
handschriftliche Notizen zu Kapitel 1: heute
Seiten 1.33–1.37;
handschriftliche Notizen zu Kapitel 2: heute Seiten 2.1—2.2 und 2.6
Weitere Lektüre:
[KS17] und
[BKS17] und [KS18]
Abschluss von Kapitel 2: Feferman-Vaught-Zerlegungen — heute:
weitere Notationen;
Formulierung und Beweis eines Lemmas, das besagt, dass jede Menge Δ in eine dazu äquivalente Menge Δ' transformiert werden kann, bei der sich die αs gegenseitig ausschließen;
Beweis des Haupt-Theorems dieses Kapitels, dass für L=FO und für L=FO+MOD Folgendes besagt: Für jede L-Formel φ und alle Variablentupel
x und y, so dass xy alle freien Variablen von φ enthält, gibt es eine Feferman-Vaught-Zerlegung von
φ bzgl. (x;y); und es gibt einen Algorithmus, der diese erzeugt;
Formulierung eines Korollars (die hierfür nötigen Definitionen finden sich am Beginn von Kapitel 3)
Material:
handschriftliche Notizen zu Kapitel 2: heute Seiten 2.3—2.15
Weitere Lektüre:
[KS18]
Start mit Kapitel 3: Gaifman-Normalform und Gaifman-Lokalität — heute:
Definition der folgenden Begriffe (inkl. Beispiele):
r-lokale Formel,
basis-lokaler Satz,
lokaler FO+MOD-Zählsatz,
Gaifman-Normalform für FO,
Gaifman-Normalform für FO+MOD;
Beispiel für einen FO-Satz φ und einen zu φ äquivalenten FO-Satz in Gaifman-Normalform;
Formulierung des Theorems über die Existenz und Berechenbarkeit von äquivalenten Formeln in Gaifman-Normalform für FO und für FO+MOD
("Satz von Gaifman für FO und FO+MOD") und Beginn des Beweises
Material:
handschriftliche Notizen zu Kapitel 3: heute Seiten 3.1–3.7
Weitere Lektüre:
[KS18]
Weiter mit Kapitel 3: Gaifman-Normalform und Gaifman-Lokalität — heute: Abschluss des Beweises des Satzes von Gaifman für FO; Beginn des Beweises des Satzes für FO+MOD
Material:
handschriftliche Notizen zu Kapitel 3: heute Seiten 3.7–3.10
Weitere Lektüre:
[KS18]
Weiter mit Kapitel 3: Gaifman-Normalform und Gaifman-Lokalität — heute: Abschluss des Beweises des Satzes von Gaifman für FO und FO+MOD (heute den Fall, dass die Formel mit einem modulo-Zählquantor beginnt, zu Ende behandelt); Feststellung, dass die im Beweis für φ konstruierte Formel γ in Gaifman-Normalform Lokalitätsradius < 7q hat, wobei q die Quantorentiefe von φ ist.
Material:
handschriftliche Notizen zu Kapitel 3: heute Seiten 3.11–3.16
Weitere Lektüre:
[KS18]
Abschluss von Kapitel 3: Gaifman-Normalform und Gaifman-Lokalität — heute: Definition der Begriffe "Anfrage" und "Gaifman-lokale Anfrage"; Nachweis der Gaifman-Lokalität aller FO+MOD-definierbaren Anfragen (unter Verwendung des Satzes von Gaifman für FO+MOD); Anwendung der Gaifman-Lokalität aller FO+MOD-definierbaren Anfragen (unter Verwendung des Satzes von Gaifman für FO+MOD) zum Nachweis, dass die folgende Anfrage nicht FO+MOD-definierbar ist: die Erreichbarkeits-Anfrage auf der Klasse aller endlichen gerichteten Graphen (Anfrage: gib alle Tupel (a,b) aus, so dass es einen Weg von Knoten a zu Knoten b gibt); Hinweise zu Feinheiten in der Definition des Begriffs "Gaifman-lokal" in verschiedenen Teilen der Fachliteratur
Material:
handschriftliche Notizen zu Kapitel 3: heute
Seiten 3.17–3.22
Weitere Lektüre:
[KS18] und [L]
und
Abschnitt 6.1–6.2 in [GS18]
und
Kapitel 10.3 im Buch [FG]
Start mit Kapitel 4: Untere Schranken an die Größe von Formeln in Normalform — heute: Kodierung von großen Zahlen durch Bäume geriner Höhe; kurze Formeln zum Vergleich von großen durch Bäume kodierte Zahlen; Formulierung und Beginn des Beweises einer unteren Schranke an die Länge von FO-Sätzen in Gaifman-Normalform
Material:
handschriftliche Notizen zu Kapitel 4: heute Seiten 4.1–4.7
Weitere Lektüre:
Kapitel 10.3 im Buch [FG];
Sections 1-4 in [DGKS07];
Corollary IV.4 in [HKS13]
Abschluss von Kapitel 4: Untere Schranken an die Größe von Formeln in Normalform — heute: Abschluss des Beweises einer unteren Schranke an die Länge von FO-Sätzen in Gaifman-Normalform; Diskussion darüber, wie der Beweis modifiziert werden kann, um Varianten des Theorems zu erhalten, die besagen "... jeder zu φh auf der Klasse aller Wälder der Höhe höchstens h äquivalente Satz in Gaifman-Normalform hat Länge mindestens Tower(h)" bzw. statt "Wälder der Höhe höchstens h" auch "Bäume"; Beweis einer unteren Schranke an die Größe von Feferman-Vaught-Zerlegungen
Material:
handschriftliche Notizen zu Kapitel 4: heute Seiten 4.7–4.13
Weitere Lektüre:
Sections 1-4 in [DGKS07];
Corollary IV.4 in [HKS13];
Section 3 in [KS18]
Start mit dem Exkurs zum Thema Baumzerlegungen und Baumweite von Graphen — heute: Notationen zu ungerichteten Graphen und Bäumen; Definition der Begriffe "Baumzerlegung eines Graphen" und "Weite einer Baumzerlegung"; viele Beispiele für Baumzerlegungen konkreter Graphen (Bäume, Kreise, Gitter); Definition des Begriffs "Baumweite eines Graphen"
Material:
handschriftliche Notizen zu Kapitel 4: heute
handschriftliche Notizen zum Exkurs "Baumzerlegungen und Baumweite von Graphen": heute Seiten B.1–B.7
Weitere Lektüre:
[D]: Kapitel 10.3 "Baumzerlegungen";
weitere Informationen und eine Charakterisierung durch das Räuber-und-Polizisten-Spiel finden sich hier.
Weiter mit dem Exkurs zum Thema Baumzerlegungen und Baumweite von Graphen — heute: Brombeersträucher, die Brombeerdicke von Graphen, viele Beispiele (Brombeersträucher für vollständige Graphen, Kreise und Gitter), ein Satzes von Seymour und Thomas zum Zusammenhang zwischen der Brombeerdicke und der Baumweite eines Graphen; Folgerung, dass ein Kreis der Länge n die Baumweite 2 hat und dass ein nxn-Gitter die Baumweite n hat
Material:
handschriftliche Notizen zu Kapitel 4: heute
Seiten B.8–B.14
Weitere Lektüre:
[FG01] und
[KS18]
Abschluss des
Exkurses zum Thema Baumzerlegungen und Baumweite von Graphen — heute:
Begriffsdefinition kleine Baumzerlegungen;
Zusammenhang zwischen der Baumweite und der Anzahl der Kanten eines Graphen;
Formulierung des Satzes von Bodlaender zur Konstruktion kleiner Baumzerlegungen minimaler Weite (ohne Beweis)
Baumzerlegungen und Baumweite von σ-Strukturen;
die Logiken MSO (monadische Logik zweiter Stufe) und CMSO (Erweiterung von MSO um modulo-Zählen);
Formulierung des Satzes von Courcelle (ohne Beweis)
Start mit Kapitel 5: Model-Checking für FO und FO+MOD auf Klassen von beschränkter lokaler Baumweite — heute: Definition des Begriffs "beschränkte lokale Baumweite";
Beispiele für Klassen von beschränkter lokaler Baumweite;
Formulierung eines algorithmischen Meta-Theorems, das besagt, dass das Problem EVALφ,C (Eingabe: eine Struktur A aus C; Frage: erfüllt A den Satz φ?) für jeden FO+MOD-Satz φ und jede Klasse C von Strukturen, die beschränkte lokale Baumweite besitzt, in Pseudo-Linearzeit gelöst werden kann — für FO wurde dies von Frick und Grohe in 2001 bewiesen; die Verallgemeinerung auf FO+MOD wurde von Kuske und Schweikardt in 2018 gezeigt — Ziel für den Rest von Kapitel 5 ist, dieses Theorem zu beweisen
Material:
handschriftliche Notizen zu Kapitel 4: heute
Seiten B.14–B.18
handschriftliche Notizen zu Kapitel 5: heute Seiten 5.1–5.3
Weitere Lektüre:
[FG01] und
[KS18]
Weiter mit Kapitel 5: Model-Checking für FO und FO+MOD auf Klassen von beschränkter lokaler Baumweite — heute: erster Meilenstein für den Beweis des algorithmischen Meta-Theorems: Definition des Begriffs einer (r,s)-Nachbarschaftsüberdeckung einer Struktur sowie Formulierung und Beginn des Beweises eines Lemmas von Peleg zur Konstruktion einer (r,2kr)-Nachbarschaftsüberdeckung
Material:
handschriftliche Notizen zu Kapitel 5: heute
Seiten 5.4–5.9 (bis zum Ende des Beweises von Behauptung 4)
Weitere Lektüre:
[FG01] und
[KS18]
Weiter mit Kapitel 5: Model-Checking für FO und FO+MOD auf Klassen von beschränkter lokaler Baumweite — heute: Abschluss des Beweises des Lemmas von Peleg zur Konstruktion einer (r,2kr)-Nachbarschaftsüberdeckung; Formulierung und Beweis eines Korollars, das besagt, dass für eine Klasse C von beschränkter lokaler Baumweite bei Eingabe einer Struktur der Größe n eine (k,2kr)-Nachbarschaftsüberdeckung der Struktur in Zeit O(n1+1/k) konstruiert werden kann; der r-Kern KrA(N) einer Menge N in einer σ-Struktur A; ein Algorithmus zur Berechnung des r-Kern KrA(N) in Zeit O(r.x), wobei x die Größe der auf N induzierten Substruktur von A ist (dabei insbes. auch die Methode der Lazy Array Initialization behandelt)
Material:
handschriftliche Notizen zu Kapitel 5: heute
Seiten 5.10–5.16
Weitere Lektüre:
[FG01] und
[KS18]
Abschluss von Kapitel 5: Model-Checking für FO und FO+MOD auf Klassen von beschränkter lokaler Baumweite — heute: Beweis von Theorem 5.3; insbesondere: ein Algorithmus, der für eine Zahl k>0, einen lokalen-FO+MOD-Zählsatz γ und eine Klasse C von beschränkter lokaler Baumweite bei Eingabe einer σ-Struktur A aus C in Zeit O(|A|1+1/k) entscheidet, ob A ⊧ γ, sowie ein Algorithmus, der für eine Zahl k>0, einen basis-lokalen FO+MOD-Satz χ und eine Klasse C von beschränkter lokaler Baumweite bei Eingabe einer σ-Struktur A aus C in Zeit O(|A|1+1/k) entscheidet, ob A ⊧ χ
Material:
handschriftliche Notizen zu Kapitel 5: heute
Seiten 5.16–5.23
Weitere Lektüre:
[FG01] und
[KS18]
Restliche Teile von Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: Wiederholung von bisher in Kapitel 1 behandelten Dingen (insbes. zu HNF-Formeln und zur effizienten Auswertung von FO(P)-Sätzen auf Klassen von Strukturen von beschränktem Grad, also Theorem 1.5 und Theorem 1.18); Beginn der Präsentation eines Linearzeit-Algorithmus für COUNTφ(x1,...,xn),d und eines Algorithmus zum Lösen von ENUMφ(x1,...,xn),d mit konstanter Taktung nach Linearzeit-Vorverarbeitung — heute: Reduktion auf den Spezialfall, in dem φ eine Sphärenformel sphτ,r(x1,...,xn) ist; Lösung für den Spezialfall, dass τ zusammenhängend ist
Material:
handschriftliche Notizen zu Kapitel 1: heute
Seiten 1.36–1.41
Weitere Lektüre:
[KS17] und
[BKS17]
Weiter mit Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: weiter mit der Präsentation eines Linearzeit-Algorithmus für COUNTφ(x1,...,xn),d und eines Algorithmus zum Lösen von ENUMφ(x1,...,xn),d mit konstanter Taktung nach Linearzeit-Vorverarbeitung — heute: Reduktion auf den Spezialfall, in dem φ(x1,...,xn) besagt, dass (x1,...,xn) ein "rainbow colored independent set" ist, d.h. dass jedes xi in der 1-stelligen Relation Ci ist und es keine Kante zwischen einem xi und einem xj gibt); Vorarbeiten zum Lösen des Zähl-Problems für diesen Spezialfall: Nutzung des Prinzip der Inklusion-Exklusion zur Reduktion auf das Zähl-Problem für Formeln αK(z1,...,zc)
Material:
handschriftliche Notizen zu Kapitel 1: heute
Seite 1.41–1.48
Weitere Lektüre:
[KS17] und
[BKS17]
Abschluss von Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: Abschluss der Präsentation eines Linearzeit-Algorithmus für COUNTφ(x1,...,xn),d; Präsentation eines Algorithmus zum Lösen von ENUMφ(x1,...,xn),d mit konstanter Taktung nach Linearzeit-Vorverarbeitung
Material:
handschriftliche Notizen zu Kapitel 1: heute
Seiten 1.48–1.58 (Korrektur: In der Behauptung auf Seite 1.53 muss in "(ai,aj)" und in "(aj,ai)" jeweils ai ersetzt werden durch ai+1)
Weitere Lektüre:
[BKS17]
Rückblick auf die in Vorlesung und Übung im Laufe des Semesters behandelten Themen; Hinweise zur Vorbereitung auf die Modulabschlussprüfung; Klären von Fragen; Feedback zum Thema Lehrevaluation