|
Logik in der Informatik
Prof. Dr. Nicole Schweikardt |
|
Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden, Tipps zum Weiterlesen und gelegentlich ergänzende Bemerkungen.
Eröffnungsveranstaltung. "Kapitel 0: Einleitung": Einführung ins Thema durch Beispiele von Formeln der Logik zweiter Stufe ("3-Färbbarkeit"), Fixpunktlogik ("Erreichbarkeit"), Logik erster Stufe (reguläre Sprache a+b*) und monadischer Logik zweiter Stufe (Sprache aller Worte, die ungerade viele a's enthalten). Klärung von Organisatorischem (entlang der Webseite der Vorlesung).
Material:
handschriftliche Notizen zu Kapitel 0.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 1.
Viele weitere Beispiele zur Bedeutung der Logik in der Informatik finden
sich in dem Artikel "On the unusual effectiveness of
logic in computer science" von Halpern, Harper, Immerman, Kolaitis, Vardi
und Vianu, Bulletin of Symbolic Logic 7(2):213-236 (2001). Eine
Vorabversion des Artikels finden Sie hier.
Start mit "Kapitel 1: Grundlagen und der Satz von Trakhtenbrot": Festlegung einiger Notationen (insbes. zu Turingmaschinen); Formulierung und Beginn des Beweises des Satzes von Trakhtenbrot.
Material:
handschriftliche Notizen zu
Kapitel 1: heute bis Seite 25.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 2.1, 2.2 und 9.1.
Abschluss von "Kapitel 1: Grundlagen und der Satz von Trakhtenbrot":
Rest des Beweises des Satzes von Trakhtenbrot.
Start mit "Kapitel 2: Die Logik zweiter Stufe und die Sätze von Büchi und
Fagin": Syntax und Semantik der Logik zweiter Stufe (SO), Beispiele für
Formeln der Logik zweiter Stufe
Material:
handschriftliche Notizen zu
Kapitel 1: heute Seiten 25 bis 29.
Teil 1 der handschriftlichen Notizen zu
Kapitel 2: heute Seiten 2.1 bis 2.6.
Übungsblatt 1.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 9.1 und 7.1.
Weiter mit "Kapitel 2: Die Logik zweiter Stufe und die Sätze von Büchi und Fagin": Beispiele für Formeln der Logik zweiter Stufe; Definition der monadischen Logik zweiter Stufe (MSO), der existentiellen Logik zweiter Stufe (ESO) und der monadischen existentiellen Logik zweiter Stufe (ESMO); Formulierung des Satzes von Büchi und Beweis der "leichten Richtung" des Satzes von Büchi ("Jede reguläre Sprache ist EMSO-definierbar")
Material:
Teil 1 der handschriftlichen Notizen zu
Kapitel 2: heute Seiten 2.7 bis 2.14
Weitere Lektüre:
Lehrbuch [L]: Kapitel 7.4.
Lehrbuch [FG]: Kapitel 10.1.
Weiter mit "Kapitel 2: Die Logik zweiter Stufe und die Sätze von Büchi und Fagin": Beweis der "schwierigen Richtung" des Satzes von Büchi ("Jede MSO-definierbare Sprache ist regulär.")
Material:
Teil 1 der handschriftlichen Notizen zu
Kapitel 2: heute Seiten 2.14 bis 2.24
Übungsblatt 2.
Weitere Lektüre:
Lehrbuch [FG]: Kapitel 10.1.
Lehrbuch [L]: Kapitel 7.4 (Beweis
mittels "MSO-Typen").
Lehrbuch [Howard Straubing: Finite Automata, Formal Logic, and Circuit
Complexity. Birkhäuser, 1994]: Kapitel III.1 (der Beweis
nutzt eine eingeschränkte Syntax und eine andere Definition der Semantik, die in Kapitel II des Buchs eingeführt werden).
Weiter mit "Kapitel 2: Die Logik zweiter Stufe und die Sätze von Büchi und Fagin": Anwendung des Satzes von Büchi zum Nachweis, dass "Hamiltonkreis" nicht MSO-definierbar ist (mittels logischer Reduktion unter Verwendung einer nicht-regulären Sprache); Definition des Begriffs der logischen Beschreibung einer Komplexitätsklasse; die Standardkodierung von Strukturen; Formulierung des Satzes von Fagin ("ESO beschreibt NP auf der Klasse aller endlichen Strukturen")
Material:
Teil 1 der handschriftlichen Notizen zu
Kapitel 2: heute Seiten 2.25 bis 2.27.
Teil 2 der handschriftlichen Notizen zu
Kapitel 2: heute Seiten 2.28 bis 2.34.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 7.4 und Kapitel 9.2.
Weiter mit "Kapitel 2: Die Logik zweiter Stufe und die Sätze von Büchi und Fagin": Beweis des Satzes von Fagin ("ESO beschreibt NP auf der Klasse aller endlichen Strukturen")
Material:
Teil 2 der handschriftlichen Notizen zu
Kapitel 2: heute Seiten 2.34 bis 2.46.
Übungsblatt 3.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 9.2.
Abschluss von "Kapitel 2: Die Logik zweiter Stufe und die Sätze von Büchi und Fagin": Wiederholung von Details zum Abschluss des Beweises des Satzes von Fagin (Aufbau der Formeln, die die Beschriftung des Bandes in der Startkonfiguration beschreiben); Beweis des Satzes von Cook und Levin (NP-Vollständigkeit des aussagenlogischen Erfüllbarkeitsproblems) unter Verwendung des Satzes von Fagin; Formulierung des Satzes von Grädel (logische Charakterisierung von P auf der Klasse aller endlichen geordneten Strukturen durch ESO-Horn Sätze
Material:
Teil 2 der handschriftlichen Notizen zu
Kapitel 2: heute Seiten 2.44 bis 2.57.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 9.2.
In [G] finden sich
u.a. Details zum Beweis des Satzes von Grädel
Start mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele": Spielregeln des Ehrenfeucht-Fraisse Spiels (kurz: EF-Spiel); partielle Isomorphismen; Beispiele zum EF-Spiel; Gewinnstrategien; das EF-Spiel auf zwei linearen Ordnungen.
Material:
Folien,
Skript zu Kapitel 3: heute Seiten 11 bis 19.
Übungsblatt 4.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 3.2.
Lehrbuch [EF]: Kapitel 2.1 bis 2.3.
Weiter mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele": Der Satz von Ehrenfeucht; Nachweis, dass die Klasse aller endlichen linearen Ordnungen gerader Länge nicht FO-definierbar ist; Beweis des Satzes von Ehrenfeucht
Material:
Folien,
Skript zu Kapitel 3: heute Seiten 20 bis 29.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 3.3 bis 3.5.
Lehrbuch [EF]: Kapitel 2.2 und 2.3.
Weiter mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele": Wiederholung der Kernideen beim Beweis des Satzes von Ehrenfeucht; Formulierung eines Korollars, das den Zusammenhang zwischen Gewinnstrategien für Duplicator, m-Äquivalenz und Hintikka-Formeln zusammenfasst; Folgerung, dass es (für jede feste, endliche, relationale Signatur) bis auf logische Äquivalenz nur endlich viele verschiedene FO-Formeln vom Quantorenrang höchstens m gibt; Kompositionslemmata (inkl. Anwendungsbeispiele) für die Vereinigung disjunkter Strukturen, für das kartesische Produkt von Strukturen und für die Konkatenation linear geordneter Strukturen; Einführung der sternfreien regulären Ausdrücke, Formulierung des Satzes von McNaughton und Papert ("sternfreie reguläre Ausdrücke beschreiben genau dieselben Wortsprachen wie Sätze der Logik erster Stufe") und Beweis der "leichten Richtung" des Satzes von McNaughton und Papert
Material:
Skript zu Kapitel 3:
heute Seite 29
Skript zu Kapitel 3:
heute Seiten 30-34
Übungsblatt 5.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 3.2 und 7.5.
Lehrbuch [EF]: Kapitel 6.4.
Weiter mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele": Beweis der "schwierigen Richtung" des Satzes von McNaughton und Papert
Material:
Skript zu Kapitel 3:
heute Seiten 34-38.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 7.5.
Lehrbuch [EF]: Kapitel 6.4.
Weiter mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele": Vorarbeiten zu "Abschnitt 3.6: Satz von Hanf": Erläuterung der Grundidee, Gaifman-Graph, Umgebungen, Nachbarschaften, Umgebungstyp, Formulierung des Satzes von Hanf (ein hinreichendes Kriterium für die Existenz einer Gewinnstrategie für Duplicator im m-Runden EF-Spiel)
Material:
handschriftliche
Notizen zum Satz von Hanf: heute Seiten 93-96.
Übungsblatt 6.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 4.1 bis 4.3.
Lehrbuch [EF]: Kapitel 2.4.
Weiter mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele": "Abschnitt 3.5: Logische Reduktionen" - heute: Nachweis, dass Graph-Zusammenhang und Erreichbarkeit nicht FO-definierbar sind; weiter mit "Abschnitt 3.6: Satz von Hanf" - heute: Beweis des Satzes von Hanf
Material:
Skript zu Kapitel 3:
heute Seiten 38-42.
handschriftliche
Notizen zum Satz von Hanf: heute Seiten 96-102.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 4.1 bis 4.3.
Lehrbuch [EF]: Kapitel 2.4 und
12.3 ("Logical Reductions").
Weiter mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele": die Hanf-Lokalität der Logik erster Stufe inkl. Anwendung zum Nachweis, dass weder Graph-Zusammenhang noch Bäume FO-definierbar sind; Hin- und Her-Systeme und der Satz von Fraisse
Material:
handschriftliche
Notizen zum Satz von Hanf: heute Seiten 102-105''
handschriftliche
Notizen zum Satz von Fraisse: heute Seiten 106-111
Übungsblatt 7.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 4.1 bis 4.3 und
Kapitel 3.5
Lehrbuch [EF]: Kapitel 2.4 und 2.3
Abschluss von "Kapitel 3: Ehrenfeucht-Fraisse Spiele": Beispiel zur Anwendung von Hin- und Her-Systemen zum Nachweis, dass Graph-Zusammenhang nicht FO-definierbar ist; das Ajtai-Fagin-Spiel zum Nachweis von Nicht-Ausdrückbarkeitsresultaten für EMSO inkl. Anwendung zum Nachweis, dass Graph-Zusammenhang nicht EMSO-definierbar ist
Material:
handschriftliche
Notizen zum Satz von Fraisse: heute Seiten 112-113
handschriftliche
Notizen zum Ajtai-Fagin-Spiel: heute Seiten 114-126.
Weitere Lektüre:
Lehrbuch [EF]: Kapitel 2.3 und
2.4 (siehe Proposition 2.4.5)
Lehrbuch [L]: Kapitel 7.3.
Start mit "Kapitel 4: 0-1-Gesetze": Einführung des Begriffs der asymptotischen Wahrscheinlichkeit; Beispiele: Berechnung der asymptotischen Wahrscheinlichkeit der Probleme EVEN ("Hat das Universum gerade Kardinalität?"), PARITY ("Enthält eine Relation gerade viele Tupel?"), ISOLATED-NODES ("Besitzt ein Graph isolierte Knoten?"), Berechnung der asymptotischen Wahrscheinlichkeit von GRAPH-ZUSAMMENHANG, Einführung des Begriffs "eine Logik L besitzt das 0-1-Gesetz bzgl. einer Klasse S von Strukturen".
Material:
handschriftliche
Notizen zu Kapitel 4: heute Seiten 86-99
Übungsblatt 8.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 12.1 und 12.2
Weiter mit "Kapitel 4: 0-1-Gesetze": Nachweis des Satzes von Glebskii et al. und Fagin, der besagt, dass FO das 0-1-Gesetz bzgl. der Klasse UG aller ungerichteten Graph besitzt (dazu wurden betrachtet: Erweiterungsaxiome für ungerichtete Graphen), und dass FO das 0-1-Gesetz bzgl. der Klasse aller σ-Strukturen (für jede endliche relationale Signatur σ) besitzt (dazu wurden eingeführt: Erweiterungsaxiome für σ-Strukturen).
Material:
handschriftliche
Notizen zu Kapitel 4: heute Seiten 100-111.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 12.1 und 12.2
Weiter mit "Kapitel 4: 0-1-Gesetze": infinitäre Logiken, k-Variablen-Logiken, Beispiele zur Ausdrucksstärke, das k-Pebble-Spiel
Material:
handschriftliche
Notizen zu Kapitel 4: heute Seiten 112-117.
Übungsblatt 9.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 8.2 und 11.1-11.2
Abschluss von "Kapitel 4: 0-1-Gesetze": das k-Pebble-Spiel; Zusammenhang zwischen k-Pebble-Spiel und Definierbarkeit in infinitärer k-Variablen-Logik; Nachweis des Satzes von Kolaitis und Vardie, der besagt, dass die infinitäre Logik mit endlich vielen Variablen das 0-1-Gesetzt bgzl. der Klasse UG aller ungerichteten Graphen und bzgl. der Klasse aller Strukturen über einer endlichen relationalen Signatur besitzt; Anwendung des 0-1-Gesetzes; Anwendung von Pebble-Spielen zum Nachweis des Satzes von de Rougemont, der besagt, dass HAMILTONKREIS nicht in infinitärer Logik mit endlich vielen Variablen definiert werden kann
Material:
handschriftliche
Notizen zu Kapitel 4: heute Seiten 117-125.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 11.2 und
12.1-12.2
In [K] finden
sich viele weitere Informationen zu infinitären Logiken, u.a. auch
Details zum Beweis des Satzes von de Rougemont
Start mit "Kapitel 5: Der Satz von Gaifman": lokale Formeln, basis-lokale Sätze und Formeln in Gaifman-Normalform; Formulierung des Satzes von Gaifman und Beginn der Beweises.
Material:
handschriftliche
Notizen zu Kapitel 5: heute Seiten 114-125.
Weitere Lektüre:
Lehrbuch [EF]: Kapitel 2.5.
Lehrbuch [L]: Kapitel 4.1-4.3.
Weiter mit "Kapitel 5: Der Satz von Gaifman": Beweis des Satzes von Gaifman
Material:
handschriftliche
Notizen zu Kapitel 5: heute Seiten 125-138.
Übungsblatt 10.
Weitere Lektüre:
Lehrbuch [EF]: Kapitel 2.5.
Lehrbuch [L]: Kapitel 4.1-4.3 und 4.5.
Weiter mit "Kapitel 5: Der Satz von Gaifman": Die Gaifman-Lokalität der Logik erster Stufe; der Satz von Seese über das Auswertungsproblem der Logik erster Stufe auf Klassen von Graphen von beschränktem Grad
Material:
handschriftliche
Notizen zu Kapitel 5: heute Seiten 139-152.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 4 und 6.6.
Abschluss von "Kapitel 5: Der Satz von Gaifman": Abschluss des Beweises des Satzes von Seese über das Auswertungsproblem der Logik erster Stufe auf Klassen von Graphen von beschränktem Grad; Ausblick auf weitere Themen (Komplexität des Auswertungsproblems für planare Graphen; untere Schranke für die Größe von Formeln in Gaifman-Normalform) Start mit "Kapitel 6: Fixpunktlogiken": Grundbegriffe (monoton, inflationär, induktiv, Fixpunkte, kleinster Fixpunkt); der Satz von Knaster und Tarski; induktive Fixpunkte
Material:
handschriftliche
Notizen zu Kapitel 5: heute Seiten 152-162.
handschriftliche Notizen zu
Kapitel 6 (alle Nummerierungen der Form "4.xy" sind hier durch "6.xy" zu ersetzen): heute: Seiten 136-138)
Übungsblatt 11.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 6.6 und 10.1
Syntax und Semantik der kleinsten Fixpuntklogik LFP und der inflationären Fixpunktlogik IFP; Beispiele für LFP-Formeln und für IFP-Formeln
Material:
handschriftliche Notizen zu
Kapitel 6 (alle Nummerierungen der Form "4.xy" sind hier durch "6.xy" zu
ersetzen): heute Seiten 139-145
Weitere Lektüre:
Lehrbuch [L]: Kapitel 10.2
der Satz von Immerman und Vardi (logische Charakterisierung von PTIME auf endlichen geordneten Strukturen durch LFP bzw. IFP)
Material:
handschriftliche Notizen zu
Kapitel 6 (alle Nummerierungen der Form "4.xy" sind hier durch "6.xy" zu
ersetzen): heute Seiten 151-154 (Theorem 4.39 inkl. Beweis)
Übungsblatt 12.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 10.4.
partielle Fixpunkte; Syntax und Semantik der partiellen Fixpunktlogik PFP; Satz von Immerman und Vardi zur logischen Charakterisierung von PSPACE durch PFP auf endlichen geordneten Strukturen; Einbettung von PFP in infinitäre Logik mit endlich vielen Variablen; Transfer der Nicht-Ausdrückbarkeitsresultate für infinitäre Logik mit endlich vielen Variablen zu Nicht-Ausdrückbarkeitsresultaten für Fixpunktlogiken (u.a.: 0-1-Gesetze)
Material:
handschriftliche Notizen zu
Kapitel 6 (alle Nummerierungen der Form "4.xy" sind hier durch "6.xy" zu
ersetzen): heute Seiten 145-150 und 154
Weitere Lektüre:
Lehrbuch [L]: Kapitel 10.4.
Lehrbuch [EF]: Kapitel 7.3, 8.3
und 8.4.
In [G] finden sich
viele Details zum Thema Fixpunklogiken.
Abschluss von "Kapitel 6: Fixpunktlogiken": Verwendung der logischen Charakterisierung von PSPACE durch PFP auf endlichen geordneten Strukturen zum Nachweis, dass die kombinierte Komplexität des Auswertungsproblems für FO PSPACE-vollständig ist; Rückblick auf die in Vorlesung und Übung im Laufe des Semesters besprochenen Themengebiete; Ausblick auf weiterführende Themen; Hinweise zum Ablauf von mündlichen Modulabschlussprüfungen
Material:
handschriftliche Notizen zu
Kapitel 6 (alle Nummerierungen der Form "4.xy" sind hier durch "6.xy" zu
ersetzen): heute Seiten 155-159 (Satz 4.44 inkl. Beweis)
Weitere Lektüre:
Lehrbuch [EF]: Kapitel 7 und
8.
Viele weitere Informationen finden sich in den Kapiteln 2 und 3 des Buchs
[F].