|
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; Einführung des Begriffs "Zählterm"
Material:
handschriftliche Notizen zu Kapitel 0: heute Seiten 0.1–0.5
Weitere Lektüre:
[KS17]
Kapitel 0: Einleitung und Grundbegriffe — heute: 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
Material:
handschriftliche Notizen zu Kapitel 0: heute Seiten 0.6–0.8
Weitere Lektüre:
[KS17]
Weiter mit Kapitel 0: Einleitung und Grundbegriffe — heute: 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 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.
Material:
handschriftliche Notizen zu Kapitel 0: heute Seiten 0.8–0.14
Weitere Lektüre:
[KS17]
Abschluss von Kapitel 0: Einleitung und Grundbegriffe — heute:
weitere einfache Beobachtungen zu Typen und Nachbarschaften.
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
Material:
handschriftliche Notizen zu Kapitel 0: heute Seite 0.15
handschriftliche Notizen zu Kapitel 1: heute Seiten 1.1–1.3
Weitere Lektüre:
[KS17]
Weiter mit Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: Formulierung und Beweis 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.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 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
Seiten 1.19–1.27
Weitere Lektüre:
[KS17]
Weiter mit Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: Anwendungen von Theorem 1.5: die Hanf-Lokalität von FO(P)
Material: handschriftliche Notizen zu Kapitel 1:
heute Seiten 1.27–1.32
Weitere Lektüre:
[KS17]
Weiter mit 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;
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.32–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); Vorüberlegungen zum Lösen des Zähl-Problems für diesen Spezialfall
Material:
handschriftliche Notizen zu Kapitel 1: heute
Seite 1.41–1.48
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: Abschluss der Präsentation eines Linearzeit-Algorithmus für COUNTφ(x1,...,xn),d; Beginn der 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.55
Weitere Lektüre:
[BKS17]
Abschluss von Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute:
Anwendungen von Theorem 1.5: algorithmische Meta-Theoreme: Abschluss der Präsentation eines Algorithmus zum Lösen von
ENUMφ(x1,...,xn),d mit konstanter Taktung nach Linearzeit-Vorverarbeitung
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; weitere Notationen;
Formulierung eines Lemmas, das besagt, dass jede Menge Δ in eine dazu äquivalente Menge Δ' transformiert werden kann, bei der sich die αs gegenseitig ausschließen
Material:
handschriftliche Notizen zu Kapitel 1: heute
Seiten 1.55–1.58 und
handschriftliche Notizen zu Kapitel 2: heute Seiten 2.1—2.3
Weitere Lektüre:
[BKS17] und [KS18]
Weiter mit Kapitel 2: Feferman-Vaught-Zerlegungen — heute: Beweis des Lemmas, das besagt, dass jede Menge Δ in eine dazu äquivalente Menge Δ' transformiert werden kann, bei der sich die αs gegenseitig ausschließen; 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.4—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; Formulierung eines Korollars (die hierfür nötigen Definitionen finden sich am Beginn von Kapitel 3)
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 und
handschriftliche Notizen zu Kapitel 3: heute 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 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; Anmerkung über den Lokalitätsradius der erzeugten äquivalenten Formel in Gaifman-Normalform
Material:
handschriftliche Notizen zu Kapitel 3: heute Seiten 3.7–3.9 und 3.15
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 Seiten 3.10–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) 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
Material:
handschriftliche Notizen zu Kapitel 3: heute
Seiten 3.17–3.22
handschriftliche Notizen zu Kapitel 4: heute Seiten 4.1–4.6
Weitere Lektüre:
[KS18] und [L]
und
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".
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 4: Untere Schranken an die Größe von Formeln in Normalform — heute:
Beweis einer unteren Schranke an die Größe von Feferman-Vaught-Zerlegungen
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 (u.a. Bäume, Kreise)
Material:
handschriftliche Notizen zu Kapitel 4: heute Seiten 4.10–4.13
und
handschriftliche Notizen zum Exkurs "Baumzerlegungen und Baumweite von Graphen": heute Seiten B.1–B.5
Weitere Lektüre:
Sections 1-4 in [DGKS07];
Corollary IV.4 in [HKS13];
Section 3 in [KS18];
[D]: Kapitel 10.3 "Baumzerlegungen"
Weiter mit dem Exkurs zum Thema Baumzerlegungen und Baumweite von Graphen — heute: weitere Beispiele für Baumzerlegungen (Gitter); Definition des Begriffs "Baumweite eines Graphen"; 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 (heute ohne Beweis); Folgerung, dass ein Kreis der Länge n die Baumweite 2 hat und dass ein nxn-Gitter die Baumweite n hat; 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)
Material:
handschriftliche Notizen zu Kapitel 4: heute
Seiten B.5–B.11 und B.14–B.17
Weitere Lektüre:
[D]: Kapitel 10.3 "Baumzerlegungen";
weitere Informationen und eine Charakterisierung durch das Räuber-und-Polizisten-Spiel finden sich hier.
Abschluss des
Exkurses zum Thema Baumzerlegungen und Baumweite von Graphen — heute:
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; 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 4: heute
Seiten B.17–B.18
handschriftliche Notizen zu Kapitel 5: heute Teil 1, Seiten 5.1–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
Material:
handschriftliche Notizen zu Kapitel 5: heute
Teil 1, Seiten 5.7–5.11
Weitere Lektüre:
[FG01] und
[KS18]