|
Logik in der Informatik
Prof. Dr. Nicole Schweikardt |
|
Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden, die in der Vorlesung verwendeten Folien, Teile des Skripts 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 (inkl. Beispiel und Übungsaufgabe), Einführung des Begriffs "Zählterm", Syntax und Semantik der Logik FO(P) (eine Erweiterung der Logik erster Stufe um unäre Zählquantoren).
Material:
handschriftliche Notizen zu Kapitel 0: heute Seiten 0.1–0.6
Weitere Lektüre:
[KS17]
Kapitel 0: Einleitung und Grundbegriffe — heute: Lösen der Übungsaufgabe, die in der letzten Vorlesung gestellt wurde; Syntax und Semantik der Logik FOC(P) (eine Erweiterung der Logik erster Stufe um Zählterme und numerische Prädikate), weitere Grundbegriffe: der Gaifman-Graph, der Grad und die Zusammenhangskomponenten einer Struktur, die Distanz zwischen Elementen im Universum einer Struktur, induzierte Substrukturen, Nachbarschaften
Material:
handschriftliche Notizen zu Kapitel 0: heute Seiten 0.7–0.10
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 (aber wichtige) Beobachtungen zu Typen und Nachbarschaften(Lemmas 0.1 bis 0.4).
Material:
handschriftliche Notizen zu Kapitel 0: heute Seiten 0.10–0.15
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 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
Teil 1, Seiten 1.1–1.3 und
Teil 2, Seite 1.4
Weitere Lektüre:
[KS17]
Weiter mit Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: Beweis von Lemma 1.6
Material:
handschriftliche Notizen zu Kapitel 1: heute Teil 2,
Seiten 1.4–1.9
Weitere Lektüre:
[KS17]
Weiter mit Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: Formulierung und Beweis des zweiten technischen Lemmas, das für den Beweis von Theorem 1.5 gebraucht wird (Lemma 1.7); Beginn des Beweises von Theorem 1.5
Material:
handschriftliche Notizen zu Kapitel 1: heute Teil 2,
Seiten 1.10–1.18
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 Logiken FO und FO+MOD
Material:
handschriftliche Notizen zu Kapitel 1: heute Teil 2,
Seiten 1.19–1.20 und Teil 3, Seite 1.21–1.27
Weitere Lektüre:
[KS17]
Weiter mit Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: Anwendungen von Theorem 1.5: Hanf-Normalform für FO+MOD; die Hanf-Lokalität von FO(P)
Material: handschriftliche Notizen zu Kapitel 1:
heute Teil
3, Seiten 1.25–1.31
Weitere Lektüre:
[KS17] und
[BKS17]
Weiter mit Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: Beispiele zur Anwendung der Hanf-Lokalität zum Nachweis der Nicht-Ausdrückbarkeit von "Graphzusammenhang" und "Planarität" in FO(P); 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)
Material:
handschriftliche Notizen zu Kapitel 1: heute
Teil 3, Seite 1.30–1.32 und
Teil 4, Seite 1.33–1.35
Weitere Lektüre:
[KS17] und
[BKS17]
Weiter mit Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: Anwendungen von Theorem 1.5: algorithmische Meta-Theoreme: 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; 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
Teil 4, Seite 1.36–1.37 und
Teil 5, Seite 1.38–1.41
Weitere Lektüre:
[KS17] und
[BKS17]
Weiter mit Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: Anwendungen von Theorem 1.5: algorithmische Meta-Theoreme: 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).
Material:
handschriftliche Notizen zu Kapitel 1: heute
Teil 5, Seite 1.41–1.46
Weitere Lektüre:
[KS17] und
[BKS17]
Weiter mit Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: Anwendungen von Theorem 1.5: algorithmische Meta-Theoreme: 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 (Lösung des Problems COUNTφ(x1,...,xn),d für den Spezialfall, in dem φ besagt, dass jedes xi in der 1-stelligen Relation Ci ist und es keine Kante zwischen einem xi und einem xj gibt; Vorüberlegung zur Lösung des Problems ENUMφ(x1,...,xn),d für diesen Spezialfall).
Material:
handschriftliche Notizen zu Kapitel 1: heute
Teil 5, Seite 1.46–1.52
Weitere Lektüre:
[BKS17]
Abschluss von Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: Anwendungen von Theorem 1.5: algorithmische Meta-Theoreme: 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 (Lösung des Problems ENUMφ(x1,...,xn),d für den Spezialfall, in dem φ besagt, dass jedes xi in der 1-stelligen Relation Ci ist und es keine Kante zwischen einem xi und einem xj gibt).
Material:
handschriftliche Notizen zu Kapitel 1: heute
Teil 5, Seite 1.52–1.57 sowie die Übungsaufgabe
Teil 6, Seite 1.58
Weitere Lektüre:
[BKS17]
Lösung der Übungsaufgabe, die am Ende von Kapitel 1 gestellt wurde. 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); weitere Notationen; Nachweis, dass jede Menge Δ in eine dazu äquivalente Menge Δ' transformiert werden kann, bei der sich die αs gegenseitig ausschließen
Material:
handschriftliche Notizen zu Kapitel 2: heute Seiten 2.1—2.5
Weitere Lektüre:
[KS18]
Weiter mit Kapitel 2: Feferman-Vaught-Zerlegungen — heute: Beweis, dass für jede FO-Formel φ und alle Variablentupel x und y, so dass xy alle freien Variablen von φ enthält, eine Feferman-Vaught-Zerlegung von φ bzgl. (x;y) berechnet werden kann; Beginn des Beweises, dass für jede FO+MOD-Formel φ und alle Variablentupel x und y, so dass xy alle freien Variablen von φ enthält, eine Feferman-Vaught-Zerlegung von φ bzgl. (x;y) berechnet werden kann.
Material:
handschriftliche Notizen zu Kapitel 2: heute Seiten 2.6—2.11
Weitere Lektüre:
[KS18]
Abschluss von Kapitel 2: Feferman-Vaught-Zerlegungen — heute:
Abschluss des Beweises, dass für jede FO+MOD-Formel φ und alle Variablentupel
x und y, so dass xy alle freien Variablen von φ enthält, eine Feferman-Vaught-Zerlegung von
φ bzgl. (x;y) berechnet werden kann.
Start mit Kapitel 3: Gaifman-Normalform und Gaifman-Lokalität — heute:
Definition des Begriffs
r-lokale Formel, Beispiele
Material:
handschriftliche Notizen zu Kapitel 2: heute Seiten 2.11—2.15
handschriftliche Notizen zu Kapitel 3: heute Teil 1, Seiten 3.1–3.2
Weitere Lektüre:
[KS18]
Weiter mit Kapitel 3: Gaifman-Normalform und Gaifman-Lokalität — heute: Definition der folgenden Begriffe: 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 Teil 1, Seiten 3.2–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
Material:
handschriftliche Notizen zu Kapitel 3: heute Teil 1, Seiten 3.7–3.9
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 der Fall, dass die Formel mit einem modulo-Zählquantor beginnt); 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 Teil 1, Seiten 3.10–3.14 und
Teil 2, Seiten 3.15–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)
Material:
handschriftliche Notizen zu Kapitel 3: heute
Teil 2, Seiten 3.16–3.20
Weitere Lektüre:
[KS18] und [L]
Übungsaufgabe:
Zeigen Sie, dass die "Diagonal-Anfrage" auf der Klasse aller Gitter (Anfrage: gib alle Knoten a aus, die auf der Diagonalen des Gitters liegen) nicht FO+MOD-definierbar ist. Hierbei ist ein Gitter ein Graph mit Knotenmenge {1,...,m}x{1,...,n}, wobei zwei Knoten (i,j) und (i',j') genau dann benachbart sind, wenn
(i=i' und |j-j'|=1) oder (j=j' und |i-i'|=1) ist. Und die Diagonale besteht aus allen Knoten der Form (i,i).
Start mit Kapitel 4: 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 (u.a. Bäume, Kreise, Gitter); Definition des Begriffs "Baumweite eines Graphen"
Material:
handschriftliche Notizen zu Kapitel 4: heute
Seiten B.1–B.7
Weitere Lektüre:
[D]: Kapitel 10.3 "Baumzerlegungen"
Übungsaufgabe:
Zeigen Sie, dass für jede positive natürliche Zahl n gilt: Jede Baumzerlegung des vollständigen Graphen Kn auf n Knoten hat Weite n-1.
Weiter mit Kapitel 4: Baumzerlegungen und Baumweite von Graphen — heute: Brombeersträucher, die Brombeerdicke von Graphen, viele Beispiele (Brombeersträucher für vollständige Graphen, Kreise und Gitter), Formulierung eines Satzes von Seymour und Thomas zum Zusammenhang zwischen der Brombeerdicke und der Baumweite eines Graphen
Material:
handschriftliche Notizen zu Kapitel 4: heute
Seiten B.8–B.11
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 Kapitel 4: Baumzerlegungen und Baumweite von Graphen — heute: Beweis des 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; kleine Baumzerlegungen
Material:
handschriftliche Notizen zu Kapitel 4: heute
Seiten B.11–B.15
Weitere Lektüre:
[D]: Kapitel 10.3 "Baumzerlegungen";
weitere Informationen und eine Charakterisierung durch das Räuber-und-Polizisten-Spiel finden sich hier.
Abschluss von Kapitel 4: Baumzerlegungen und Baumweite von Graphen — heute:
kleine Baumzerlegungen; Zusammenhang zwischen der Baumweite und der Anzahl der Kanten eines Graphen;
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 Bodlaender zur Konstruktion kleiner Baumzerlegungen (ohne Beweis); 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"
Material:
handschriftliche Notizen zu Kapitel 4: heute
Seiten B.14–B.18
handschriftliche Notizen zu Kapitel 5: heute Teil 1, Seiten 5.1–5.2
Weitere Lektüre:
[D]: Kapitel 10.3 "Baumzerlegungen"
(weitere Informationen und eine Charakterisierung durch das Räuber-und-Polizisten-Spiel finden sich hier) und
[FG01]
Weiter mit Kapitel 5: Model-Checking für FO und FO+MOD auf Klassen von beschränkter lokaler Baumweite — heute: 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; erster Meilenstein im Beweis: 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
Teil 1, Seiten 5.2–5.7
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
Material:
handschriftliche Notizen zu Kapitel 5: heute
Teil 1, Seiten 5.4–5.12
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: der r-Kern KrA(N) einer Menge N in einer σ-Struktur A und ein Algorithmus zur dessen Berechnung in Zeit O(r.x), wobei x die Größe der auf N induzierten Substruktur von A ist; 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 ⊧ γ
Material:
handschriftliche Notizen zu Kapitel 5: heute
Teil 2, Seiten 5.x–5.y
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: 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 ⊧ χ; Abschluss des Beweises des algorithmischen Meta-Theorems, das besagt, dass das Problem EVALφ,C für einen FO+MOD-Satz φ, eine Klasse C von beschränkter lokaler Baumweite und eine beliebige Zahl k>0 bei Eingabe einer Struktur A aus C in Zeit O(|A|1+1/k) gelöst werden kann
Material:
handschriftliche Notizen zu Kapitel 5: heute
Teil 2, Seiten 5.y–5.z
Weitere Lektüre:
[FG01] und
[KS18]
Start mit Kapitel 6: 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
Material:
handschriftliche Notizen zu Kapitel 6: heute Seiten 4.1–4.6
Weitere Lektüre:
Abschnitt 6.1–6.2 in [GS18]
und
Kapitel 10.3 im Buch [FG]
Weiter mit Kapitel 4: Untere Schranken an die Größe von Formeln in Normalform — heute: Formulierung und Beweis 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", "ungerichtete Wälder der Höhe höchstens h", "ungerichtete Bäume".
Material:
handschriftliche Notizen zu Kapitel 4: heute Seiten 4.6–4.9
Weitere Lektüre:
Kapitel 10.3 im Buch [FG];
Sections 1-4 in [DGKS07];
Corollary IV.4 in [HKS13]
Abschluss von Kapitel 6: Untere Schranken an die Größe von Formeln in Normalform — heute:
Beweis einer unteren Schranke an die Größe von Feferman-Vaught-Zerlegungen
Hinweise zur Vorbereitung auf eine mündliche Modulabschlussprüfung
Material:
handschriftliche Notizen zu Kapitel 6: heute Seiten 4.10–4.13
Weitere Lektüre:
Sections 1-4 in [DGKS07];
Corollary IV.4 in [HKS13];
Section 3 in [KS18]