|
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.
Weiter mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele" — heute: 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); Definition und Korrektheitsnachweis des Ajtai-Fagin-Spiels
Material:
handschriftliche
Notizen zum Satz von Hanf: heute Seiten 100-105''.
handschriftliche
Notizen zum Ajtai-Fagin-Spiel und zum Beweis, dass Graph-Zusammenhang nicht EMSO-definierbar ist: heute Seiten 114-118 (bis zum Ende des Beweises von Satz 3.44).
Weitere Lektüre:
Lehrbuch [L]: Kapitel 4.1 bis 4.3.
Lehrbuch [EF]: Kapitel 2.4.
Weiter mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele" — heute: ein EMSO-Satz, der das Komplement von Graph-Zusammenhang definiert; Verwendung des Ajtai-Fagin-Spiels zum Beweis, dass Graph-Zusammenhang nicht EMSO-definierbar ist; Bemerkung zur Äquivalenz der Ausdrucksstärke von MSO und FO für relationale Signaturen, die nur Relationssymbole der Stelligkeit 1 enthalten (Übungsaufgabe)
Material:
handschriftliche
Notizen zum Ajtai-Fagin-Spiel und zum Beweis, dass Graph-Zusammenhang nicht EMSO-definierbar ist: heute Seiten 118-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)
Weiter mit "Kapitel 3: Ehrenfeucht-Fraisse Spiele" — heute: Hin- und Her-Systeme und der Satz von Fraisse (heute bei Satz 3.40 nur den Beweis der Richtungen "(a)=>(b)" und "(b)=>(c)" behandelt); 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-109 und 111-113
Weitere Lektüre:
Lehrbuch [EF]: Kapitel 2.3
Lehrbuch [L]: Kapitel 3.5
Abschluss von Kapitel 3: Ehrenfeucht-Fraisse Spiele" — heute: Beweis der Richtung "(c)=>(a)" von Satz 3.40 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?") und PARITY ("Enthält eine Relation gerade viele Tupel?"); Einführung des Begriffs "eine Logik L besitzt das 0-1-Gesetz bzgl. einer Klasse S von Strukturen"
Material:
handschriftliche
Notizen zum Satz von Fraisse: heute Seiten 109-111
handschriftliche
Notizen zu Kapitel 4: heute Seiten 86-89 und 94
Weitere Lektüre:
Lehrbuch [L]: Kapitel 12.1 und 12.2
Weiter mit "Kapitel 4: 0-1-Gesetze" — heute: Weitere Beispiele: Berechnung der asymptotischen Wahrscheinlichkeit des Problems ISOLATED-NODES ("Besitzt ein Graph isolierte Knoten?"), Berechnung der asymptotischen Wahrscheinlichkeit von GRAPH-ZUSAMMENHANG in der Klasse UG aller ungerichteten Graphen; die Erweiterungsaxiome EAl,m und EAk := EA2k,k für ungerichtete Graphen; Nachweis, dass die asymptotische Wahrscheinlichkeit von EAk und von EAl,m in UG genau 1 ist; Beispiel zur Anwendung des Satzes (zur Berechnung der asymptotischen Wahrscheinlichkeit von ISOLATED-NODES in der Klasse UG);
Material:
handschriftliche
Notizen zu Kapitel 4: heute Seiten 89-101
Weitere Lektüre:
Lehrbuch [L]: Kapitel 12.1 und 12.2
Weiter mit "Kapitel 4: 0-1-Gesetze" — heute: weitere Beispiele zur Anwendung des Satzes (zur Berechnung der asymptotischen Wahrscheinlichkeit von GRAPH-ZUSAMMENHANG und TRIANGLE ("Besitzt ein Graph ein Dreieck?" in der Klasse UG); Formulierung und 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; Formulierung 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 Logik (inkl. Beispiele zur Ausdrucksstärke)
Material:
handschriftliche
Notizen zu Kapitel 4: heute Seiten 102-113.
Weitere Lektüre:
Lehrbuch [L]: Kapitel 8.2 und 11.1-11.2
Weiter mit "Kapitel 4: 0-1-Gesetze" — heute: k-Variablen-Logiken (inkl. Beispiele zur Ausdrucksstärke dieser Logiken); das k-Pebble-Spiel; Zusammenhang zwischen k-Pebble-Spiel und Definierbarkeit in infinitärer k-Variablen-Logik
Material:
handschriftliche
Notizen zu Kapitel 4: heute Seiten 113-118.
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:
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;
Start mit "Kapitel 5: Fixpunktlogiken" — heute:
Grundbegriffe (monoton,
inflationär, Fixpunkte, kleinster Fixpunkt);
der Satz von Knaster und Tarski
Material:
handschriftliche
Notizen zu Kapitel 4: heute Seiten 118-125;
handschriftliche Notizen zu
Kapitel 5 (alle Nummerierungen der Form "4.xy" sind hier durch "5.xy" zu ersetzen): heute: Seiten 136-137
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
Lehrbuch [L]: Kapitel 10.1 und 10.2
Weiter mit "Kapitel 5: Fixpunktlogiken" — heute: Nachtrag zum Beweis des Satzes von Knaster und Tarski: die im Beweis definierte Menge M ist nicht-leer, da insbes. X:=A ein Element in M ist; Induktionsstufen, induktive Abbildungen und induktive Fixpunkte; der Operator Fφ,R; Syntax und Semantik der monotonen Fixpunktlogik MFP und der kleinsten Fixpunktlogik LFP; Beispiele für LFP-Formeln
Material:
handschriftliche Notizen zu
Kapitel 5 (alle Nummerierungen der Form "4.xy" sind hier durch "5.xy" zu ersetzen): heute: Seiten 137-142
Weitere Lektüre:
Lehrbuch [L]: Kapitel 10.1 und 10.2
Weiter mit "Kapitel 5: Fixpunktlogiken" — heute: inflationäre Fixpunkte; Syntax und Semantik der inflationären Fixpunktlogik IFP; Beispiele für Formeln; partielle Fixpunkte; ein Beispiel
Material:
handschriftliche Notizen zu
Kapitel 5 (alle Nummerierungen der Form "4.xy" sind hier durch "5.xy" zu
ersetzen): heute Seiten 142-146
Weitere Lektüre:
Lehrbuch [L]: Kapitel 10.2
Weiter mit "Kapitel 5: Fixpunktlogiken" — heute: 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); Aussage und Beweisidee zum Satz von Immerman und Vardi (logische Charakterisierung von PTIME auf endlichen geordneten Strukturen durch LFP bzw. IFP)
Material:
handschriftliche Notizen zu
Kapitel 5 (alle Nummerierungen der Form "4.xy" sind hier durch "5.xy" zu
ersetzen): heute Seiten 146-154
Weitere Lektüre:
Lehrbuch [L]: Kapitel 10.4.
Hinweise zum Ablauf von mündlichen Modulabschlussprüfungen; Rückblick auf die in Vorlesung und Übung im Laufe des Semesters besprochenen Themengebiete; Besprechung der Ergebnisse der Lehrevaluation