|
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: 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, 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
Material:
handschriftliche Notizen zu Kapitel 0: heute Seiten 0.7–0.13
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: Verallgemeinerung des Satzes von Seese zur
Linearzeit-Auswertung von FO-Sätzen auf Strukturen vom Grad höchstens d für FO(P) statt FO, sowie
Verdeutlichung am Beispiel "k-Clique auf Graphen vom Grad höchstens d" für festes k
Material:
handschriftliche Notizen zu Kapitel 0: heute Seiten 0.13–0.15
handschriftliche Notizen zu Kapitel 1: heute Teil 1
Weitere Lektüre:
[KS17]
Algorithmische Anwendungen der schwachen Hanf-Normalform: Auswerten einer Formel über einer Interpretation. Lemma zur Vereinfachung von Booleschen Kombinationen von Sphärenformeln (siehe auch Lemma 5.2 in [BKS17]). Diskussion zum Aufzählen der Ergebnisrelation mit konstanter Verzögerung durch das Auswerten von Sphärenformeln.
Weiter mit Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: Skizze zum Beweis von Theorem 1.5; 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 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); Beweis von Theorem 1.5; direkte Folgerungen aus dem Beweis (Radius der HNF-Formel und Laufzeit zur Konstruktion der Formel)
Material:
handschriftliche Notizen zu Kapitel 1: heute Teil 2,
Seiten 1.10–1.20 und Teil 3, Seite 1.21–1.22
Weitere Lektüre:
[KS17]
Weiter mit Kapitel 1: Hanf-Normalform und Hanf-Lokalität — heute: Anwendungen von Theorem 1.5: Hanf-Normalform für die Logiken FO und FO+MOD; die Hanf-Lokalität von FO(P)
Material:
handschriftliche Notizen zu Kapitel 1: heute Teil 3, Seiten 1.23–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: Linearzeit-Algorithmus zum Lösen des Problems EVALφ,d für einen beliebigen FO(P)-Satz φ und eine Gradschranke d; 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; 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
Material:
handschriftliche Notizen zu Kapitel 1: heute
Teil 4, Seite 1.33–1.37
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 (Reduktion des allgemeinen Problems auf 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.38–1.??
Weitere Lektüre:
[KS17] und
[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 der beiden Probleme 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.?–1.??
Weitere Lektüre:
[BKS17]
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). Nachweis, 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.
Material:
handschriftliche Notizen zu Kapitel 2: heute Seiten 2.1—2.2 und 2.6—2.10
Weitere Lektüre:
[KS18]
Weiter mit Kapitel 2: Feferman-Vaught-Zerlegungen — heute: 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.3—2.5 und 2.11—2.13
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 der folgenden Begriffe:
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")
Material:
handschriftliche Notizen zu Kapitel 2: heute Seiten 2.13—2.15
handschriftliche Notizen zu Kapitel 3: heute Teil 1, Seiten 3.1–3.4
Weitere Lektüre:
[KS18]
Weiter mit Kapitel 3: Gaifman-Normalform und Gaifman-Lokalität — heute: Beginn des Beweises des Satzes von Gaifman für FO und FO+MOD
Material:
handschriftliche Notizen zu Kapitel 3: heute Teil 1, Seiten 3.5 und 3.10–3.14 und 3.6–3.8
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; 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)
Material:
handschriftliche Notizen zu Kapitel 3: heute Teil 1, Seiten 3.8–3.9 und
Teil 2, Seiten 3.15–3.20
Weitere Lektüre:
[KS18]
Weiter mit Kapitel 3: Gaifman-Normalform und Gaifman-Lokalität — heute:
Anwendung der Gaifman-Lokalität aller FO+MOD-definierbaren Anfragen (unter
Verwendung des Satzes von Gaifman für FO+MOD) zum Nachweis, dass die folgenden Anfragen nicht FO+MOD-definierbar sind:
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) und die Diagonal-Anfrage auf der Klasse aller Gitter (Anfrage: gib alle Knoten a aus, die auf der Diagonalen des Gitters liegen);
Beginn des Abschnitts zur Anwendung des Satzes von Gaifman zum Nachweis von algorithmischen Meta-Theoremen:
Einführung der Begriffe Baumweite, lokale Baumweite, Klassen von beschränkter lokaler Baumweite, sowie Beispiele (Baumweite eines Pfads, eines Kreises, eines Graphen, eines Gitters; Nachweis, dass für jede natürliche Zahl d die Klasse aller Graphen vom Grad höchstens d lokal beschränkte Baumweite besitzt); 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)
Material:
handschriftliche Notizen zu Kapitel 3: heute
Teil 2, Seiten 3.20–3.22 und
Exkurs zum Thema Baumzerlegungen, Seiten B.1–B.7 und
Teil 3, Seiten 3.23–3.?
Weitere Lektüre:
[FG01] und
[KS18] und
[D]: Kapitel 10.3 "Baumzerlegungen"
Weiter mit Kapitel 3: Gaifman-Normalform und Gaifman-Lokalität — heute: Beginn des Beweises des algorithmischen Meta-Theorems für FO und FO+MOD: Grundstruktur des Algorithmus, ein Lemma von Peleg zur effizienen Konstruktion von Nachbarschaftsüberdeckungen
Material:
handschriftliche Notizen zu Kapitel 3: heute
Teil 3, Seiten 3.?–?
Weitere Lektüre:
[FG01] und
[KS18]
Weiter mit Kapitel 3: Gaifman-Normalform und Gaifman-Lokalität — heute: Abschluss des Beweises des algorithmischen Meta-Theorems für FO und FO+MOD: kleine Baumzerlegungen, eine obere Schranke an die Größe von Graphen der Baumweite höchstens w, ein Algorithmus zur Konstruktion des r-Kerns einer Knotenmenge, ein Algorithmus zur Auswertung von basis-lokalen Sätzen, Formulierung (ohne Beweis) einer Variante des Satzes von Courcelle, die besagt, dass es für jede Zahl w und jede CMSO-Formel ψ(x) einen Linearzeit-Algorithmus gibt, der bei Eingabe einer Struktur A der Baumweite höchsten w die Menge aller a in A berechnet, so dass (A,a) die Formel ψ erfüllt
Material:
Exkurs zum Thema Baumzerlegungen, Seiten B.14–B.18
und handschriftliche Notizen zu Kapitel 3: heute Teil 3, Seiten 3.?–?
Weitere Lektüre:
[FG01] und
[KS18] und
[D]: Kapitel 10.3 "Baumzerlegungen"
Nachtrag zum Thema Baumzerlegungen und Baumweite von Graphen: Brombeersträucher, die Brombeerdicke von Graphen, ein Satz von Seymour und Thomas zum Zusammenhang zwischen der Brombeerdicke und der Baumweite eines Graphen, und der Nachweis, dass das nxn-Gitter die Baumweite n hat
Material:
handschriftliche Notizen: heute
Exkurs zum Thema Baumzerlegungen, Seiten B.8–B.14
Weitere Lektüre:
[D]: Kapitel 10.3 "Baumzerlegungen"
Weiter mit Kapitel 3: Gaifman-Normalform und Gaifman-Lokalität — heute: Basis-lokale Sätze und cl-Terme: Einführung des Begriffs cl-Term, Überlegungen zur effizienten Auswertung von cl-Termen, Beginn des Beweises zur Übersetzung von basis-lokalen Sätzen in cl-Terme
Material:
handschriftliche Notizen zu Kapitel 3: heute Teil 5, Seiten 3.?–3.?
Weitere Lektüre:
[GS18] (Abschnitt 6.1–6.2)
Abschluss von Kapitel 3: Gaifman-Normalform und Gaifman-Lokalität — heute:
Abschluss des Beweises zur Übersetzung von basis-lokalen Sätzen in cl-Terme
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
Material:
handschriftliche Notizen zu Kapitel 3: heute Teil 5, Seiten 3.?–3.?
handschriftliche Notizen zu Kapitel 4: heute Seiten 4.1–4.2
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: 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.3–4.8
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; Beweis einer unteren Schranke an die Größe von Feferman-Vaught-Zerlegungen
Material:
handschriftliche Notizen zu Kapitel 4: heute Seiten 4.8–4.13
Weitere Lektüre:
Sections 1-4 in [DGKS07];
Corollary IV.4 in [HKS13];
Section 3 in [KS18]