|
Logik in der Informatik
Prof. Dr. Nicole Schweikardt |
|
Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden, die in der Vorlesung verwendeten Folien, 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).
Start mit "Kapitel 1: Grundlagen und der Satz von Trakhtenbrot" — heute:
Festlegung einiger Notationen (insbes. zu Turingmaschinen);
Formulierung des Satzes von Trakhtenbrot.
Material:
handschriftliche Notizen zu Kapitel 0 (aus dem SoSe 2015)
handschriftliche Notizen zu Kapitel 1: Seiten 10-13 und 17
(pdf-Seiten 1-4 und 8)
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.
Weiter mit "Kapitel 1: Grundlagen und der Satz von Trakhtenbrot" — heute: Festlegung weiterer Notationen bzgl. Turingmaschinen; Beginn des Beweises des Satzes von Trakhtenbrot.
Material:
handschriftliche Notizen zu
Kapitel 1: Seiten 13-16 und 18-27 (pdf-Seiten 4-7 und 9-18).
Übungsblatt 1
Weitere Lektüre:
Lehrbuch [L]: Kapitel 2.1, 2.2 und 9.1.
Abschluss von "Kapitel 1: Grundlagen und der Satz von Trakhtenbrot" — heute:
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), der monadischen Logik zweiter Stufe (MSO), der
existentiellen Logik zweiter Stufe (ESO) und der existentiellen monadischen Logik zweiter Stufe (EMSO),
Beispiele für Formeln dieser Logiken
Material:
handschriftliche Notizen zu
Kapitel 1: Seiten 27-29 (pdf-Seiten 18-20)
Teil 1 der handschriftliche Notizen zu
Kapitel 2: Seiten 2.1-2.8 (pdf-Seiten 1-8)
Übungsblatt 2
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" — heute: 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.9 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" — heute: 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 3
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
Weiter mit "Kapitel 2: Die Logik zweiter Stufe und die Sätze von Büchi und Fagin" — heute: 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 und Beginn des Beweises 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.43.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 7.4 und Kapitel 9.2.
Abschluss von "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"); 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.43 bis 2.57.
Übungsblatt 4.
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" — heute: Spielregeln des Ehrenfeucht-Fraisse Spiels (kurz: EF-Spiel); partielle Isomorphismen; Beispiele zum EF-Spiel; Gewinnstrategien; das EF-Spiel auf zwei linearen Ordnungen; der Satz von Ehrenfeucht (inkl. Beweis); Nachweis, dass die Klasse aller endlichen linearen Ordnungen gerader Länge nicht FO-definierbar ist; Hintikka-Formeln; 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
Material:
Folien 1-29,
Skript Seiten 11-29
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: 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 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 zu Kapitel 3:
heute Seiten 30-38 (bis zum Ende des Beweises von Behauptung (*))
Ü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" — heute: Abschluss des Beweises des Satzes von McNaughton und Papert; 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": 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) und Beginn des Beweises
Material:
Skript zu Kapitel 3:
heute Seiten 38-42.
handschriftliche
Notizen zum Satz von Hanf: heute Seiten 93-99.
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: Abschluss des Beweises des Satzes von Hanf; die Hanf-Lokalität der Logik erster Stufe inkl. Anwendung zum Nachweis, dass Graph-Zusammenhang nicht FO-definierbar ist
Material:
handschriftliche
Notizen zum Satz von Hanf: heute Seiten 100-105.
Ü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" — heute: Anwendung der Hanf-Lokalität der Logik erster Stufe zum Nachweis, dass Bäume nicht FO-definierbar sind; Anwendung des Satzes von Hanf zum Nachweis, dass Graph-Zusammenhang nicht EMSO-definierbar ist; Anmerkungen zum Ajtai-Fagin-Spiel
Material:
handschriftliche
Notizen zum Satz von Hanf: heute Seiten 102-105''
handschriftliche
Notizen zum Ajtai-Fagin-Spiel und zum Beweis, dass Graph-Zusammenhang nicht EMSO-definierbar ist: heute Seiten 114-116 und 119-126.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 4.1 bis 4.3 und Kapitel 7.3 (zur Anwendung des Satzes von Hanf bzw. der Hanf-Lokalität von FO zum Nachweis, dass Graph-Zusammenhang nicht EMSO-definierbar ist)
Lehrbuch [EF]: Kapitel 2.4 (siehe Proposition 2.4.5)
Abschluss von "Kapitel 3: Ehrenfeucht-Fraisse Spiele" — heute: Hin- und Her-Systeme und der Satz von Fraisse; Beispiel zur Anwendung von Hin- und Her-Systemen zum Nachweis, dass Graph-Zusammenhang nicht FO-definierbar ist
Material:
handschriftliche
Notizen zum Satz von Fraisse: heute Seiten 106-113
Übungsblatt 7.
Weitere Lektüre:
Lehrbuch [EF]: Kapitel 2.3
Lehrbuch [L]: Kapitel 3.5
Start mit "Kapitel 4: 0-1-Gesetze" — heute: 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 in der Klasse UG aller ungerichteten Graphen; Einführung des Begriffs "eine Logik L besitzt das 0-1-Gesetz bzgl. einer Klasse S von Strukturen"; die Erweiterungsaxiome EAl,m und EAk := EA2k,k für ungerichtete Graphen; Beginn des Beweises von Satz 4.4 ("die asymptotische Wahrscheinlichkeit von EAk in UG ist 1")
Material:
handschriftliche
Notizen zu Kapitel 4: heute Seiten 86-99
Weitere Lektüre:
Lehrbuch [L]: Kapitel 12.1 und 12.2
Weiter mit "Kapitel 4: 0-1-Gesetze" — heute: Abschluss des Beweises von Satz 4.4; Beispiele zur Anwendung des Satzes (zur Berechnung der asymptotischen Wahrscheinlichkeit von ISOLATED-NODES, GRAPH-ZUSAMMENHANG und TRIANGLE ("Besitzt ein Graph ein Dreieck?") in der Klasse UG; Beweis des Satzes von Glebskii et al. und Fagin, der besagt, dass FO das 0-1-Gesetz bzgl. der Klasse UG aller ungerichteten Graph besitzt
Material:
handschriftliche
Notizen zu Kapitel 4: heute Seiten 99-107.
Übungsblatt 8.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 12.1 und 12.2
Weiter mit "Kapitel 4: 0-1-Gesetze" — heute: Formulierung und Beweis des Satzes von Glebskii et al. und Fagin, der besagt, 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); infinitäre Logiken, k-Variablen-Logiken, Beispiele zur Ausdrucksstärke dieser Logiken
Material:
handschriftliche
Notizen zu Kapitel 4: heute Seiten 108-114.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 8.2 und 11.1-11.2
Weiter mit "Kapitel 4: 0-1-Gesetze" — heute: 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 115-125.
Übungsblatt 9.
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
Abschluss von "Kapitel 4: 0-1-Gesetze" — heute: der Rado-Graph: Definition des Rado-Graphen inkl. der Beobachtung, dass der Rado-Graph alle Erweiterungsaxiome erfüllt; die Entscheidbarkeit der Theorie des Rado-Graphen; ein Algorithmus, der bei Eingabe eines FO[E]-Satzes φ die asymptotische Wahrscheinlichkeit von φ in UG berechnet
Material:
handschriftliche
Notizen zu Kapitel 4: heute Seiten 126-135.
Weitere Lektüre:
Lehrbuch [L]: Kapitel
12.3
Start mit "Kapitel 5: Fixpunktlogiken": Grundbegriffe (monoton, inflationär, induktiv, Fixpunkte, kleinster Fixpunkt); der Satz von Knaster und Tarski; induktive Fixpunkte; der Operator Fφ,R; Syntax und Semantik der monotonen Fixpunktlogik
Material:
handschriftliche Notizen zu
Kapitel 5 (alle Nummerierungen der Form "4.xy" sind hier durch "5.xy" zu ersetzen): heute: Seiten 136-140)
Übungsblatt 10.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 10.1 und 10.2
Weiter mit "Kapitel 5: Fixpunktlogiken": 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 5 (alle Nummerierungen der Form "4.xy" sind hier durch "5.xy" zu
ersetzen): heute Seiten 140-145
Weitere Lektüre:
Lehrbuch [L]: Kapitel 10.2
Weiter mit "Kapitel 5: Fixpunktlogiken": partielle Fixpunkte; Syntax und Semantik der partiellen Fixpunktlogik PFP; der Satz von Immerman und Vardi (logische Charakterisierung von PTIME auf endlichen geordneten Strukturen durch LFP bzw. IFP): Beginn des Beweises
Material:
handschriftliche Notizen zu
Kapitel 6 (alle Nummerierungen der Form "4.xy" sind hier durch "5.xy" zu
ersetzen): heute Seiten 145-147 und 151-152
Übungsblatt 11.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 10.4.
Weiter mit "Kapitel 5: Fixpunktlogiken": der Satz von Immerman und Vardi (logische Charakterisierung von PTIME auf endlichen geordneten Strukturen durch LFP bzw. IFP): Abschluss des Beweises; Beweis des Satzes von Vardi zur logischen Charakterisierung von PSPACE auf endlichen geordneten Strukturen durch PFP
Material:
handschriftliche Notizen zu
Kapitel 5 (alle Nummerierungen der Form "4.xy" sind hier durch "5.xy" zu
ersetzen): heute Seiten 151-155
Weitere Lektüre:
Lehrbuch [L]: Kapitel 10.4.
Weiter mit "Kapitel 5: Fixpunktlogiken": 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 (0-1-Gesetze, Pebble-Spiele); Einbettung von LFP in Logik zweiter Stufe
Material:
handschriftliche Notizen zu
Kapitel 5 (alle Nummerierungen der Form "4.xy" sind hier durch "5.xy" zu
ersetzen): heute Seiten 148-150;
Lehrbuch [EF]: Kapitel 8.5 ("Fixed-Point Logics and Second-Order Logic")
Weitere Lektüre:
Lehrbuch [L]: Kapitel 11.1.
Lehrbuch [EF]: Kapitel 8.4 und 8.5
In [G] finden sich
viele Details zum Thema Fixpunklogiken.
Abschluss von "Kapitel 5: Fixpunktlogiken":
Details zur offenen Forschungsfrage nach einer "Logik für PTIME".
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:
Kapitel 3.1.4 "The Quest for a Logic Capturing Polynomial Time" im Buch
Descriptive Complexity, Canonisation, and Definable Graph Structure Theory, Martin Grohe, Lecture Notes in Logic, Volume 47. Cambridge University Press, 2017. LINK.
Martin Grohe, The quest for a logic capturing PTIME.
In Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS'08), pp.267-271, 2008. LINK.
Weitere Lektüre:
Buch
Descriptive Complexity, Canonisation, and Definable Graph Structure Theory, Martin Grohe, Lecture Notes in Logic, Volume 47. Cambridge University Press, 2017. LINK.