|
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]
Weiter mit Kapitel 5: Model-Checking für FO und FO+MOD auf Klassen von beschränkter lokaler Baumweite — heute: 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
Material:
handschriftliche Notizen zu Kapitel 5: heute
Teil 1, Seiten 5.11–5.12; ab der Definition von KrA(N) bis zum Ende von Kapitel 5 sind z.Zt. leider keine handschriftlichen Notizen verfügbar — hier sind Sie auf Ihre eigene Mitschrift während der Vorlesung angewiesen
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: 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; 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:
ab der Definition von KrA(N) bis zum Ende von Kapitel 5 sind z.Zt. leider keine handschriftlichen Notizen verfügbar — hier sind Sie auf Ihre eigene Mitschrift während der Vorlesung angewiesen
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 ⊧ χ; dies schließt den Beweis des algorithmischen Meta-Theorems ab, 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:
ab der Definition von KrA(N) bis zum Ende von Kapitel 5 sind z.Zt. leider keine handschriftlichen Notizen verfügbar — hier sind Sie auf Ihre eigene Mitschrift während der Vorlesung angewiesen
Weitere Lektüre:
[FG01] und
[KS18]
Rückblick auf die in Vorlesung und Übung im Laufe des Semesters behandelten Themen; Hinweise zur Vorbereitung auf die Modulabschlussprüfung; Feedback zum Thema Lehrevaluation
Material: Hinweis zu einem Lösungsansatz, um eine Variante von Theorem 4.7 für FO+MOD statt FO zu bekommen: Wir sind hier etwas bescheidener, so dass es uns reicht, die folgende Aussage zu beweisen.
Es gibt eine Folge von FO+MOD-Sätzen (φh)h=1,2,..., so dass für jede elementare Funktion f gilt: Für jedes hinreichend große h gibt es keinen zu φh äquivalenten FO+MOD-Satz in GNF der Länge < f(h), der äquivalent zu φh ist.
Lösungsansatz:
Als φh wähle einen FO-Satz, so dass für alle natürlichen Zahlen m,n < Tower(h) gilt:
Die Disjunkte Vereinigung der Bäume T(m) und T(n) erfüllt genau dann den Satz φh, wenn gilt: m ≠ n.
Mit den in Kapitel 4 bereitgestellten Mitteln kann man dies leicht durch FO-Sätze der Länge O(h) ausdrücken.
Der Rest des Beweises ist durch Widerspruch. Wir betrachten hinreichend große Zahlen h und nehmen an, es gäbe einen zu φh äquivalenten FO+MOD-Satz ψh der Länge höchstens f(h). Danach kann man sich dann ein kombinatorisches Argument ausdenken, aus dem man Zahlen m ≠ n mit m,n < Tower(h) erhält, so dass T(m) und T(n) genau dieselben FO+MOD-Sätze der Länge höchstens 2 f(h) erfüllen. Und danach kann man sich weitere Argumente überlegen, mit denen man letztendlich zeigt, dass die disjunkte Vereinigung von 2 Kopien von T(m) den Satz ψh genau dann erfüllt, wenn die disjunkte Vereinigung von T(m) und T(n) den Satz ψh erfüllt.
Fragestunde zur Unterstützung der Vorbereitung auf die Modulabschlussprüfung.
Überblick über ein Resultat, das zeigt, dass basis-lokale Sätze ausgedrückt werden können durch eine Aussage der Art g>0, wobei g ein so genannter connected local term ist.
Material: Die Characterisierung von basis-lokalen Sätzen durch connected local terms findet sich in der Arbeit [GS18] (siehe Abschnitte 6.1 und 6.2 in der ArXiv-Version von [GS18]).