Mi, 14.04.04 (Nicole Schweikardt):
Organisatorisches, Kapitel 0: Einleitung, Anfang von Kapitel 1: Grundlagen.
Folien.
Tabelle
der "Artikel"-Relation aus der Beispiel-Datenbank von Kapitel 0.
Fr., 16.4.2004 (Stephan Kreutzer):
Abschnitt 1.2: Einführung in die
Komplexitätstheorie. Einführung des verwendeten
Turing-Maschinen-Modells, sowie der wichtigsten
Komplexitätsklassen und der von ihnen gebildeten
Hierarchie. Die Vorlesung endete kurz hinter Korollar 1.22.
Anmerkung: Das hier begonnene und am Mittwoch
fortgesetzte Kapitel über Komplexitätstheorie soll
Ihnen nur einen Überblick über einige wichtige
Ergebnisse der Komplexitätstheorie geben, sowie Ihnen ein
Gefühl für Komplexitätsklassen und ihre
Anordnung vermitteln. Sie brauchen die einzelnen Sätze, deren
Beweise größtenteils auch nicht gegeben werden, nicht im
einzelnen zu verstehen.
Mi., 21.4.2004:
Abschluß der Einführung in die
Komplexitätstheorie. Beginn des Kapitels über die
Komplexität der Logik erster Stufe.
Fr., 23.4.2004:
Auswertungsalgorithmus für die Logik erster Stufe;
Definition verschiedener Komplexitätsmaße.
Mi., 28.4.2004:
Satz von Trakhtenbrot mit Anwendungen. Kapitel 1 damit beendet.
Fr., 30.4.2004:
Kapitel 2: Deskriptive Komplexität. Begriff des
Beschreibens von Komplexitätsklassen
eingeführt. Logik zweiter Stufe definiert mit
Beispielen. Satz von Fagin.
Mi., 5.5.2004:
Keine Vorlesung wegen Tag der Informatik
Fr., 7.5.2004:
Satz von Fagin zu Ende
bewiesen. Kapitel 2.2: Fixpunktlogiken angefangen und Satz von
Knaster und Tarski bewiesen.
Mi., 12.5.2004:
Umstieg auf Folienvorlesung. Kleinste,
inflationäre und partielle Fixpunktlogik eingeführt und anhand
von Beispielen illustriert. Satz von Immerman und Vardi
bewiesen.
Fr., 14.5.2004:
Transitive Hüllenlogik definiert und
mittels Beispielen illustriert. Einige Varianten eingeführt
(DTC, posDTC, posTC). Bewiesen, daß DTC Logspace und TC
NLogspace beschreibt. Satz von Immerman und Szelepcsényi bewiesen.
Mi., 19.5.2004:
Beschreibungen von Komplexitätsklassen
auf ungeordneten Strukturen. Kanonisierung und Definierbarkeit von
Ordnungen.
Fr., 21.5.2004:
Interpretationen behandelt.
Interpretationen als logische Reduktionen und Kanonisierung durch
Interpretationen. Einführung in die Spiele von
Ehrenfeucht und Fraissé. Definition der m-Äquivalenz und der
Hintikka-Formeln.
Mi., 26.5.2004:
Definition der
Ehrenfeucht-Fraissé-Spiele. Charakterisierung der m-Äquivalenz
durch Hintikka-Formeln, Hin- und Her-Systeme und m-Isomorphie. Die Sätze von
Ehrenfeucht, Hintikka und Fraissé. Einige Beispiele.
Fr., 28.5.2004:
Wiederholung der Spielmethode von
Ehrenfeucht und Fraissé. Definition des Gaifman-Graphen und der Satz
von Hanf.
Mi., 2.6.2004 (Nicole Schweikardt):
Hanf-Lokalität von FO-axiomatisierbaren Klassen.
Gaifman-Lokalität von FO-definierbaren Anfragen.
Mi., 9.6.2004:
Ein EF-Spiel für die existentielle Logik zweiter Stufe.
Das Ajtai-Fagin-Spiel für die monadische existentielle Logik zweiter Stufe.
Start mit dem Beweis des Satzes, dass Graphzusammenhang in monadischer universeller Logik
zweiter Stufe, nicht aber in monadischer existentieller Logik zweiter Stufe
definiert werden kann.
Fr., 11.6.2004:
Beweis, dass Graphzusammenhang
nicht in monadischer existentieller Logik zweiter Stufe
definiert werden kann.
Einführung der k-Variablen Logik FO^k und der infinitären k-Variablen Logik.
Einige Beispiele für Formeln dieser Logiken.
Beweis, dass zwei endliche Strukturen genau dann dieselben Sätze der infinitären
k-Variablen Logik erfüllen, wenn sie dieselben FO^k-Sätze erfüllen.
Einführung von Pebble-Spielen.
Mi., 16.6.2004:
Einige Beispiele zu Pebble-Spielen. Charakterisierung der
Äquivalenz bzgl. infinitären k-Variablen Formeln durch Pebble-Spiele und durch
k-partielle Isomorphie. Beweis, dass es keine Formel der infinitären k-Variablen Logik
gibt, die die Klasse aller Graphen, die einen Hamiltonpfad haben, definiert.
Folien zur
Charakterisierung der infinitären k-Variablen Logik durch
Pebble-Spiele.
Fr., 18.6.2004:
Definition der k-Invarianten A/k einer Struktur A. Beweis, dass
zwei Strukturen A und B genau dann dieselben Sätze der infinitären k-Variablen Logik
erfüllen, wenn ihre k-Invarianten A/k und B/k isomorph sind.
Beginn mit Kapitel 5: Fixpunktlogiken. Beweis, dass jede PFP-Formel zu einer
Formel der infinitären k-Variablen Logik äquivalent ist. Folien
zur Definition der k-Invarianten einer Struktur.
Mi., 23.6.2004:
Vorarbeiten zum Beweis des Satzes von Abiteboul und Vianu.
Folien (heute bis incl. Lemma 5.8 gekommen).
Mi., 30.6.2004:
Schluss vom Beweis des Satzes von Abiteboul und Vianu.
Simultane kleinste Fixpunktlogik S-LFP eingeführt. Gezeigt, dass der simultane kleinste Fixpunkt zweier
Operatoren auch als geschachtelter einfacher Fixpunkt geschrieben werden kann.
Fr., 2.7.2004:
Gezeigt, dass LFP genauso ausdrucksstark wie S-LFP ist.
Mit dem Beweis des Stage Comparison Theorems angefangen.
Mi., 7.7.2004 (1. Vorlesung):
Schluss vom Beweis des Stage Comparison Theorems.
Beweis des Satzes von Gurevich und Shelah (IFP = LFP auf der Klasse aller endlichen Strukturen).
Beweis von Immermans Normalform für LFP. Folien.
Mi., 7.7.2004 (2. Vorlesung; an Stelle der Übungsstunde):
Gezeigt, dass das Auswertungsproblem für FO (also die kombinierte Komplexität des
FO-Model-Checking Problems) PSPACE-vollständig ist.
Beginn mit Kapitel 6: Baumautomaten. Bottom-up Baumautomaten und
reguläre Baumsprachen eingeführt.
Fr., 9.7.2004: Satz von Thatcher und Wright bzw. Doner für reguläre Baumsprachen gezeigt.
Satz von Büchi für reguläre Wortsprachen daraus gefolgert. Als eine Anwendung davon gefolgert, dass
die Klasse aller linear geordneten Graphen, die einen Hamiltonpfad besitzen, nicht MSO-definierbar ist.
Abschließendes Beispiel, wie XML-Dokumente als Bäume und DTDs als Beschreibung regulärer
Baumsprachen aufgefasst werden können.
