|
Logik in der Informatik
Prof. Dr. Nicole Schweikardt |
|
Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden, die entsprechenden Teile des Skripts und gelegentlich auch Korrekturen und sonstige 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 (aus dem SoSe 2015);
die in der Vorlesung verwendeten Folien bzw. Teile des Vorlesungsskripts (heute bis zum Ende von 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" — heute: Festlegung einiger Notationen (insbes. zu Turingmaschinen); Formulierung des Satzes von Trakhtenbrot; Beginn des Beweises des Satzes von Trakhtenbrot.
Material:
handschriftliche Notizen zu Kapitel 1: Seiten 10-19 und 21-22;
die in der Vorlesung verwendeten Folien bzw. Teile des Vorlesungsskripts (heute alle Folien bis zum Ende von Kapitel 1; und Skript-Seiten 11-17)
Weitere Lektüre:
Lehrbuch [L]: Kapitel 2.1, 2.2 und 9.1.
Abschluss von "Kapitel 1: Grundlagen und der Satz von Trakhtenbrot" — heute:
Abschluss des Beweises des Satzes von Trakhtenbrot.
Start mit "Kapitel 2: Die Logik zweiter Stufe und die Sätze von Büchi und
Fagin": — heute: Syntax der Logik zweiter Stufe (SO)
Material:
handschriftliche Notizen zu
Kapitel 1: Seiten 20-29 (pdf-Seiten 11-20)
Teil 1 der handschriftlichen Notizen zu
Kapitel 2: heute Seiten 2.1 bis 2.4 (pdf-Seiten 1-4)
die in der Vorlesung verwendeten Folien bzw. Teile des Vorlesungsskripts (heute bis inkl. Folie 33; und Skript-Seiten 17-25)
Weitere Lektüre:
Lehrbuch [L]: Kapitel 9.1 und 7.4
Nachtrag zum Beweis des Satzes von Trakhtenbrot: Verwendung des aufsteigenden Satzes von Löwenheim und Skolem zum Nachweis, dass es (für den Fall, dass M bei leerer Eingabe nicht anhält) keinen FO-Satz phiM gibt, der die Struktur AM bis auf Isomorphie exakt beschreibt.
Weiter mit "Kapitel 2: Die Logik zweiter Stufe und die Sätze von Büchi und
Fagin": — heute: Semantik der Logik zweiter Stufe (SO); Beispiele für SO-Formeln;
Definition der monadischen Logik zweiter Stufe (MSO), der
existentiellen Logik zweiter Stufe (ESO) und der existentiellen monadischen Logik zweiter Stufe (EMSO);
Formulierung des Satzes von Büchi
Material:
Teil 1 der handschriftlichen Notizen zu
Kapitel 2: heute Seiten 2.5 bis 2.11 (pdf-Seiten 5-11)
die in der Vorlesung verwendeten Folien bzw. Teile des Vorlesungsskripts (heute bis inkl. Folie 46; und Skript-Seiten 25-30)
Weitere Lektüre:
Lehrbuch [L]: Kapitel 7.4.
Lehrbuch [FG]: Kapitel 10.1.
Beweis der "leichten Richtung" des Satzes von Büchi ("Jede reguläre Sprache ist EMSO-definierbar"); Beginn des Beweises 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.12 bis 2.19 (pdf-Seiten 12-19)
die in der Vorlesung verwendeten Folien bzw. Teile des Vorlesungsskripts (heute bis inkl. Folie 51; und Skript-Seiten 31-36)
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).
Informationen zu Anwendungen der "Automatentheoretischen Methode" (analog zum Beweis der "schwierigen Richtung" des Satzes von Büchi finden sich in Section 6 des Artikels "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). Einen Überblick und weitere
Literaturhinweise gibt auch die Arbeit "Logik und Automaten: ein echtes Dreamteam" von Björklund, Martens, Schweikardt und Schwentick, Informatik Spektrum 33(5): 452-461 (2010) LINK
Abschluss des Beweises der "schwierigen Richtung" des Satzes von Büchi ("Jede MSO-definierbare Sprache ist regulär."); Ausblick auf weitere Resultate zur Ausdrucksstärke von (Fragmenten von) MSO auf Worten, Bäumen und Graphen: u.a. Beweisidee dazu, wie man zeigen kann, dass jede reguläre Sprache sogar duch einen ESO-Satz beschrieben werden kann, der nur eine einzige Mengenvariable nutzt.
Material:
Teil 1 der handschriftlichen Notizen zu
Kapitel 2: heute Seiten 2.15 bis 2.25
die in der Vorlesung verwendeten Folien bzw. Teile des Vorlesungsskripts (heute bis inkl. Folie 54; und Skript-Seiten 36-39)
Weitere Lektüre:
Details zum Beweis dazu, warum man für jeden DFA sogar einen dazu äquivalenten EMSO-Satz konstruieren kann, der nur eine einzige Mengenvariable nutzt, finden sich in Satz 2.0.1 der Arbeit "Logische Klassifizierung regulärer Baumsprachen" von Andreas Potthoff, Bericht Nr. 9410, August 1994, Christian-Albrechts-Universität Kiel.
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).
Informationen zu Anwendungen der "Automatentheoretischen Methode" (analog zum Beweis der "schwierigen Richtung" des Satzes von Büchi finden sich in Section 6 des Artikels "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). Einen Überblick und weitere
Literaturhinweise gibt auch die Arbeit "Logik und Automaten: ein echtes Dreamteam" von Björklund, Martens, Schweikardt und Schwentick, Informatik Spektrum 33(5): 452-461 (2010) LINK
Weiter mit "Kapitel 2: Die Logik zweiter Stufe und die Sätze von Büchi und
Fagin" — heute:
weitere Details zur Beweisidee dazu, wie man zeigen kann, dass jede reguläre Sprache sogar duch einen ESO-Satz beschrieben werden kann, der nur eine einzige Mengenvariable nutzt;
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 (pdf-Seiten 1-7)
die in der Vorlesung verwendeten Folien bzw. Teile des Vorlesungsskripts (heute bis inkl. Folie 64; und Skript-Seiten 39-45)
Weitere Lektüre:
Details zum Beweis dazu, warum man für jeden DFA sogar einen dazu äquivalenten EMSO-Satz konstruieren kann, der nur eine einzige Mengenvariable nutzt, finden sich in Satz 2.0.1 der Arbeit "Logische Klassifizierung regulärer Baumsprachen" von Andreas Potthoff, Bericht Nr. 9410, August 1994, Christian-Albrechts-Universität Kiel.
Lehrbuch [FG]: Kapitel 10.1.
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" — heute: Beginn des Beweises 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.41 (pdf-Seiten 7-14)
Weitere Lektüre:
Lehrbuch [L]: Kapitel 9.2.
Weiter mit "Kapitel 2: Die Logik zweiter Stufe und die Sätze von Büchi und Fagin" — heute: Abschluss des Beweises 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.41 bis 2.47 (pdf-Seiten 14-20)
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" — heute: 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.52 bis 2.57 (pdf-Seiten 25-30);
Weitere Lektüre:
Lehrbuch [L]: Kapitel 9.2.
In [Grädel] finden sich
u.a. Details zum Beweis des Satzes von Grädel.
Start mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele" — heute: Spielregeln des Ehrenfeucht-Fraisse Spiels (kurz: EF-Spiel); partielle Isomorphismen; Beispiele zum EF-Spiel; Gewinnstrategien; das EF-Spiel auf zwei linearen Ordnungen; Formulierung des Satzes von Ehrenfeucht
Material:
Skript-Fragment Seiten 11-20 (d.h. die ersten 10 Seiten der pdf-Datei), bis inkl. Folie 18 (siehe auch Folien 1-18)
Weitere Lektüre:
Lehrbuch [L]: Kapitel 3.2 bis 3.5.
Lehrbuch [EF]: Kapitel 2.1 bis 2.3.
Weiter mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele" — heute: Beweis des Satzes von Ehrenfeucht – dafür auch behandelt: Hintikka-Formeln; Nachweis, dass die Klasse aller endlichen linearen Ordnungen gerader Länge nicht FO-definierbar ist
Material:
Skript-Fragment Seiten 20-29 (d.h. die Seiten 10-19 der pdf-Datei), bis inkl. Folie 28 (siehe auch Folien 18-28)
Weitere Lektüre:
Lehrbuch [L]: Kapitel 3.2 bis 3.5.
Lehrbuch [EF]: Kapitel 2.1 bis 2.3.
Weiter mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele" — heute: 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-Sätze vom Quantorenrang höchstens m gibt; Kompositionslemmata (inkl. Anwendungsbeispiel) für die Vereinigung disjunkter Strukturen und für das kartesische Produkt von Strukturen; Kompositionslemma für die Konkatenation linear geordneter Strukturen; Einführung der sternfreien regulären Ausdrücke, Beispiele, Formulierung und Beginn des Beweises des Satzes von McNaughton und Papert ("sternfreie reguläre Ausdrücke beschreiben genau dieselben Wortsprachen wie Sätze der Logik erster Stufe")
Material:
Skript-Fragment Seiten 29-34, bis inkl. Folie 39
(siehe auch Folien 29-39)
Weitere Lektüre:
Lehrbuch [L]: Kapitel 3.2 und 7.5.
Lehrbuch [EF]: Kapitel 6.4.
Weiter mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele" — heute: Fortführung des Beweises des Satzes von McNaughton und Papert ("sternfreie reguläre Ausdrücke beschreiben genau dieselben Wortsprachen wie Sätze der Logik erster Stufe"): Abschluss des Beweises der Richtung "=>"; Beginn des Beweises der Richtung "<="
Material:
Skript-Fragment Seiten 34-36, bis inkl. Folie 43
(siehe auch Folien 39-43)
Weitere Lektüre:
Lehrbuch [L]: Kapitel 3.2 und 7.5.
Lehrbuch [EF]: Kapitel 6.4.
Weiter mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele" — heute: Abschluss des Beweises des Satzes von McNaughton und Papert ("sternfreie reguläre Ausdrücke beschreiben genau dieselben Wortsprachen wie Sätze der Logik erster Stufe"): Abschluss des Beweises der Richtung "<="
Material:
Skript-Fragment Seiten 36-38, bis inkl. Folie 44
(siehe auch Folien 39-43)
Weitere Lektüre:
Lehrbuch [L]: Kapitel 3.2 und 7.5.
Lehrbuch [EF]: Kapitel 6.4.
Weiter mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele" — heute: Erläuterung der Grundidee zu "logischen Reduktionen" anhand eines Beispiels (Nachweis, dass Graph-Zusammenhang und Erreichbarkeit nicht FO-definierbar sind); Vorarbeiten zum "Satz von Hanf": 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:
Skript-Fragment Seiten 38-42 (bis zum Ende der pdf-Datei)
handschriftliche
Notizen zum Satz von Hanf: heute Seiten 93-96.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 7.5 und Kapitel 4.1 bis 4.3.
Lehrbuch [EF]: Kapitel 6.4, Kapitel 2.4 und Kapitel 12.3 ("Logical Reductions").
Weiter mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele" — heute: Beweis des Satzes von Hanf
Material:
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.