| Mo, 11.4.11: |
Skript S. 1-9: Beispiele (Logik als Datenbankanfragen, Logik zur Charakterisierung von Komplexitätsklassen, Logiken zur Hardware- und Prozessspezifikation und Verifikation), allgemeine Notationen, Strukturen, Syntax der Logik erster Stufe |
| Mi, 13.4.11: |
Skript S. 10-15: Semantik der Logik erster Stufe; Isomorphielemma; Turing-Maschinen; Unentscheidbarkeit des Halteproblems |
| Mo, 18.4.11: |
Skript S. 16-20: Zeit- und Platzklassen; Vollständigkeit;
eine alternative Charakterisierung der Klasse NP |
| Mi, 20.4.11: |
Skript S. 21-26: Kodierung von Formeln und Strukturen;
kombinierte Komplexität und Datenkomplexität
des Auswertungsproblems für FO;
Beweis des Satzes von Trakhtenbrot bis einschließlich Schritt 2
|
| Mi, 27.4.11: |
Skript S. 26-33: Ende des Beweises des Satzes von Trakhtenbrot;
Anwendungen des Satzes von Trakhtenbrot am Beispiel
der Ordnungsinvarianz von FO-Formeln im Endlichen;
Beginn von Kapitel 4: Grundlegende Definitionen,
Definierbarkeit endlicher Strukturen bis auf Isomorphie,
Quantorenrang, m-Äquivalenz,
Proposition 4.8 inkl. Beweis
|
| Mo, 02.5.11: |
Skript S. 33-37: partielle Isomorphismen;
Ehrenfeucht-Fraïssé-Spiele eingeführt;
Beispiele; Satz 4.14 bewiesen;
erwähnt, dass entweder Spoiler oder Duplicator
eine Gewinnstrategie im Ehrenfeucht-Fraïssé-Spiel
besitzt
|
| Mi, 04.5.11: |
Skript S. 37-41:
Satz von Ehrenfeucht bewiesen;
Beispiele für nicht FO-definierbare Klassen von Strukturen;
logische Reduktionen
|
| Mo, 09.5.11: |
Skript S. 42-46:
Satz von Hanf bewiesen
|
| Mi, 11.5.11: |
Skript S. 46-50:
vereinfachte Version des Satzes von Hanf;
Hanf-Lokalität der Logik erster Stufe;
Vorbereitungen zum Satz von Gaifman;
Satz von Gaifman angegeben und
den Beweis bis einschließlich Fall 1 im Induktionsschritt besprochen
|
| Mo, 16.5.11: |
Skript S. 50-52:
Satz von Gaifman bewiesen
|
| Mi, 18.5.11: |
Skript S. 52-55:
Beweis des Satzes von Gaifman beendet;
untere Schranke für den Grössenunterschied
von FO-Formeln zu äquivalenten FO-Formeln in GNF;
Gaifman-Lokalität;
Nichtdefinierbarkeit von Grapherreichbarkeit
in der Logik erster Stufe via Gaifman-Lokalität
|
| Mo, 23.5.11: |
Skript S. 57-62:
Logik zweiter Stufe;
existentielle Logik zweiter Stufe;
Satz von Fagin angegeben
und den Beweis bis einschließlich Schritt 1 besprochen
|
| Mi, 25.5.11: |
Skript S. 61-65:
Ende vom Beweis des Satzes von Fagin;
EF-Spiele für ESO bis einschließlich Beweis von Satz 5.8
|
| Mo, 30.5.11: |
fand nicht statt |
| Mi, 1.6.11: |
fand nicht statt |
| Mo, 6.6.11: |
Skript S. 66-70:
Ajtai-Fagin-Spiele und monadische existentielle Logik zweiter Stufe;
Abschnitt 6.1 angefangen:
(kleinste) Fixpunkte;
monotone Abbildungen;
Beginn des Beweises des Satzes von Knaster und Tarski
bis einschließlich Schritt 1
|
| Mi, 8.6.11: |
Skript S. 70-74:
Abschluss des Beweises des Satzes von Knaster und Tarski;
induktive Abbildungen und Fixpunkte;
Berechnung induktiver Fixpunkte;
Zusammenfall des kleinsten und des induktiven Fixpunkts
für monotone Abbildungen;
Definition der Syntax und Semantik der kleinsten Fixpunktlogik
|
| Mi, 15.6.11: |
Skript S. 74-77:
Beispiele zu LFP;
Datenkomplexität von LFP;
inflationäre Fixpunktlogik;
Satz von Immerman und Vardi angegeben,
Beweis bis einschließlich der Hinrichtung
|
| Mo, 20.6.11: |
Skript S. 77-80:
Satz von Immerman und Vardi bewiesen;
partielle Fixpunkte definiert;
Proposition 6.31 bewiesen
|
| Mi, 22.6.11: |
Skript S. 81-87:
Beispiel zu partiellen Fixpunkten;
partielle Fixpunktlogik (PFP) eingeführt
und gezeigt, dass PFP PSPACE auf FINORD beschreibt;
Satz 6.38 wurde nicht behandelt;
TC- und DTC-Logik eingeführt bis einschließlich Beispiel 6.42
|
| Mo, 27.6.11: |
Skript S. 87-91:
Übersetzung von DTC-Formeln in TC-Formeln;
Charakterisierung von LOGSPACE und NLOGSPACE
durch die positiven Fragmente von DTC und TC;
Übersetzung von DTC-Formeln in positive DTC-Formeln
|
| Mi, 29.6.11: |
Skript S. 91-94:
Übersetzung von TC-Formeln in positive DTC-Formeln
|
| Mo, 4.7.11: |
Skript S. 94-98:
NLOGSPACE=co-NLOGSPACE via Charakterisierung von NLOGSPACE durch TC;
Infinitäre Logik L∞ω;
Endliche-Variablen-Fragmente von FO und L∞ω;
Pebble-Spiele (Motivation)
|
| Mi, 6.7.11: |
Skript S. 99-103:
Pebble-Spiele eingeführt;
Charakterisierung der Ausdrucksstärke von
L∞ωk durch k-Pebble-Spiele;
Striktheit der k-Variablen-Hierarchie bzgl.
L∞ω;
Zusammenfall von FOk-Äquivalenz
und L∞ωk-Äquivalenz
für endliche Strukturen
|
| Mo, 11.7.11: |
Skript S. 103-106:
Striktheit der k-Variablen-Hierarchie bzgl. FO;
EVEN nicht L∞ωω-definierbar
in FIN;
Satz von de Rougemont: Die Klasse der stark zusammenhängenden,
gerichteten Graphen mit einem Hamilton-Pfad ist nicht
L∞ωω-definierbar
in der Klasse der stark zusammenhängenden, gerichteten Graphen;
Einbettung von PFP in L∞ωω;
L∞ωω ist echt stärker
als PFP auf FINORD
|
| Mo, 11.7.11: |
Skript S. 106/107, 113/114:
Korollar 7.21 und 7.22;
Satz von Abiteboul und Vianu angegeben, aber nicht bewiesen;
Überblick über die in der Vorlesung behandelten
Charakterisierungen von Komplexitätsklassen
auf geordneten Strukturen;
Relationen von Logiken zu Komplexitätsklassen auf
endlichen (möglicherweise ungeordneten) Strukturen
|
