|
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)
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-20
(pdf-Seiten 1-11)
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.
Material:
handschriftliche Notizen zu
Kapitel 1: Seiten 20-29 (pdf-Seiten 11-20)
Weitere Lektüre:
Lehrbuch [L]: Kapitel 9.1
Start mit "Kapitel 2: Die Logik zweiter Stufe und die Sätze von Büchi und Fagin": — heute: Syntax und Semantik der Logik zweiter Stufe (SO); Beispiele für SO-Formeln
Material:
Teil 1 der handschriftlichen Notizen zu
Kapitel 2: heute Seiten 2.1 bis 2.7 (pdf-Seiten 1-7)
Weitere Lektüre:
Lehrbuch [L]: Kapitel 7.4.
Lehrbuch [FG]: Kapitel 10.1.
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 und 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.7 bis 2.15
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
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 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.33 (pdf-Seiten 1-6)
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" — heute: Beispiel einer ESO-Formel, die den transitiven und reflexiven Abschluss der Kantenrelation eines Graphen definiert; 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.33 bis 2.44 (pdf-Seiten 6-17)
Weitere Lektüre:
Lehrbuch [L]: Kapitel 9.2.
In [G] finden sich
u.a. Details zum Beweis des Satzes von Grädel
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"); Beweis des Satzes von Cook und Levin (NP-Vollständigkeit des aussagenlogischen Erfüllbarkeitsproblems) unter Verwendung des Satzes von Fagin
Material:
Teil 2 der handschriftlichen Notizen zu
Kapitel 2: heute Seiten 2.44 bis 2.51 (pdf-Seiten 17-24)
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:
Formulierung des Satzes von Grädel
(logische Charakterisierung von P auf der Klasse aller endlichen
geordneten Strukturen durch ESO-Horn Sätze)
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:
Teil 2 der handschriftlichen Notizen zu
Kapitel 2: heute Seiten 2.52 bis 2.57 (pdf-Seiten 25-30);
Folien 1-18 und
Skript Seiten 11-20 (pdf-Seiten 1-10)
Weitere Lektüre:
Lehrbuch [L]: Kapitel 9.2.
In [Grädel] finden sich
u.a. Details zum Beweis des Satzes von Grädel.
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; 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
Material:
Folien 18-33 und
Skript Seiten 11-31
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: Kompositionslemma 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 31-36
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); Motivation zum "Satz von Hanf"
Material:
Skript zu Kapitel 3:
heute Seiten 36-41
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: 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:
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; Anwendung der Hanf-Lokalität der Logik erster Stufe zum Nachweis, dass Bäume nicht FO-definierbar sind (Beweisidee)
Material:
handschriftliche
Notizen zum Satz von Hanf: heute Seiten 100-105''.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 4.1 bis 4.3.
Lehrbuch [EF]: Kapitel 2.4.
Weiter mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele" — heute: Ajtai-Fagin-Spiel und Beweis, dass Graph-Zusammenhang nicht EMSO-definierbar ist
Material:
handschriftliche
Notizen zum Ajtai-Fagin-Spiel und zum Beweis, dass Graph-Zusammenhang nicht EMSO-definierbar ist: heute Seiten 114-124.
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: Formulierung eines Satzes, der besagt, dass auf unären Signaturen FO die gleiche Ausdrucksstärke wie MSO hat; 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 Ajtai-Fagin-Spiel und zum Beweis, dass Graph-Zusammenhang nicht EMSO-definierbar ist: heute Seiten 124-126.
handschriftliche
Notizen zum Satz von Fraisse: heute Seiten 106-113
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
Material:
handschriftliche
Notizen zu Kapitel 4: heute Seiten 86-95
Weitere Lektüre:
Lehrbuch [L]: Kapitel 12.1 und 12.2
Weiter mit "Kapitel 4: 0-1-Gesetze" — heute: Nachweis, dass die asymptotische Wahrscheinlichkeit von EAk in UG genau 1 ist; 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 96-107
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 auch 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-115.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 8.2 und 11.1-11.2
Abschluss von "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 Vardi, der besagt, dass die infinitäre Logik mit endlich vielen Variablen das 0-1-Gesetzt bzgl. 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.
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: 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
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; Ausblick
Material:
handschriftliche Notizen zu
Kapitel 5 (alle Nummerierungen der Form "4.xy" sind hier durch "5.xy" zu
ersetzen): heute Seiten 141-145
Weitere Lektüre:
Lehrbuch [L]: Kapitel 10.2
Weiter mit "Kapitel 5: Fixpunktlogiken" — heute: der Satz von Immerman und Vardi (logische Charakterisierung von PTIME auf endlichen geordneten Strukturen durch LFP bzw. IFP); Ausblick auf den Satz 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-154
Weitere Lektüre:
Lehrbuch [L]: Kapitel 10.4.
Abschluss von "Kapitel 5: Fixpunktlogiken": partielle Fixpunkte; Syntax und Semantik der partiellen Fixpunktlogik PFP; 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)
Material:
handschriftliche Notizen zu
Kapitel 5 (alle Nummerierungen der Form "4.xy" sind hier durch "5.xy" zu
ersetzen): heute Seiten 145-150
Weitere Lektüre:
Lehrbuch [L]: Kapitel 10.4.
Besprechung der Ergebnisse der Lehrevaluation; 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; Beantwortung von Fachfragen zu einzelnen in Vorlesung bzw. Übung behandelten Themen