Aktueller Eintrag

Logbuch: Logik in der Informatik

Vorlesung  im WS 2011/12

Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden sowie gelegentlich ergänzende Bemerkungen.


Di, 25.10.2011
Eröffnungsveranstaltung. Einführung ins Thema und Klärung von Organisatorischem. Definition der Begriffe "Signatur" und "Struktur"; Beispiele für Strukturen; Festlegung einiger Notationen; Definition des Begriffs "Isomorphismus"; Beispiele für Isomorphismen.
Material:
Skript Kapitel 0 und Kapitel 1 bis inkl. Satz 1.12.
Weitere Lektüre:
Kapitel 1 und Kapitel 3.1 in [EFT]. Einen Überblick über die Rolle der Logik in der Informatik gibt [HHIKVV]; der Artikel ist online hier verfügbar. Einen Einblick in die Geschichte der logischen Grundlagen der Mathematik gibt der Comic [Logicomix]; weitere Informationen dazu finden Sie hier.
Do, 27.10.2011, 14h15-15h45
Syntax und Semantik der Logik erster Stufe; Beispiele.
Material:
Skript Kapitel 1 bis inkl. Beispiel 1.29.
Weitere Lektüre:
Kapitel 2 und Kapitel 3.2, 3.3 und 3.6 in [EFT].
Do, 27.10.2011, 16h15-17h45
Koinzidenzlemma; Isomorphielemma; Äquivalenz und Folgerung; Substitutionen.
Übungsblatt 1 ausgeteilt.
Material:
Skript Kapitel 1 bis inkl. Beispiel 1.43 und Kapitel 2 bis inkl. Beobachtung 2.2.
Weitere Lektüre:
Kapitel 3.4, 3.5 und 3.8 in [EFT].
Di, 01.11.2011
Substitutionslemma; pränexe Normalform; termreduzierte Formeln; relationale Signaturen.
Material:
Skript Rest von Kapitel 1 und Kapitel 2 (komplett).
Weitere Lektüre:
Kapitel 3.8, 8.1 und 8.4 in [EFT].
Do, 03.11.2011
Auswertungskomplexität der Logik erster Stufe auf endlichen Strukturen; Spielregeln des Ehrenfeucht-Fraisse Spiels (kurz: EF-Spiel); Beispiele zum EF-Spiel.
Übungsblatt 2 ausgeteilt.
Material:
Skript Kapitel 3 (komplett) und Kapitel 4 (bis inkl. Beispiel 4.3).
Weitere Lektüre:
Kapitel 4.2 und 4.3 in [FG], Kapitel 6.1, 6.2, 6.5 und 3.2 in [L]. Insbesondere enthält Kapitel 6.5 von [L] einen Beweis der PSPACE-Vollständigkeit des Auswertungproblems für FO auf FIN.
Di, 08.11.2011
EF-Spiele: Gewinnbedingung, Gewinnstrategien, das EF-Spiel auf zwei linearen Ordnungen
Material:
Kapitel 4 (bis inkl. Satz 4.11).
Weitere Lektüre:
Kapitel 3.2 in [L], Kapitel 2.1 bis 2.3 in [EF].
Do, 10.11.2011
Der Satz von Ehrenfeucht; Methode zum Nachweis, dass bestimmte Klassen von Strukturen nicht FO-definierbar sind; Nachweis, dass die Klasse aller endlichen linearen Ordnungen gerader Länge nicht FO-definierbar ist
Übungsblatt 3 ausgeteilt.
Material:
Kapitel 4 (bis inkl. Satz 4.21).
Weitere Lektüre:
Kapitel 3.3, 3.4 und 3.5 in [L], Kapitel 2.1 bis 2.3 in [EF].
Di, 15.11.2011
Gewinnstrategien für Spoiler; logische Reduktionen; Vorarbeiten zum Satz von Hanf (Gaifman-Graph, r-Nachbarschaft, r-Umgebungstyp)
Material:
Kapitel 4 (bis inkl. Definition 4.28).
Weitere Lektüre:
Kapitel 3.4, 3.6 und 4.1 in [L], Kapitel 2.1 bis 2.4 und 12.3 ("Logical Reductions") in [EF].
Do, 17.11.2011
Der Satz von Hanf; die Hanf-Lokalität der Logik erster Stufe
Übungsblatt 4 ausgeteilt.
Material:
Kapitel 4 (bis inkl. Satz 4.30).
Weitere Lektüre:
Kapitel 4.1 bis 4.3 in [L], Kapitel 2.4 in [EF].
Di, 22.11.2011
die Hanf-Lokalität der Logik erster Stufe; Hin- und Her-Systeme; der Satz von Fraisse
Material:
Kapitel 4 (komplett).
Weitere Lektüre:
Kapitel 4.1-4.3 und 3.5-3.6 in [L], Kapitel 2.4 und 2.3 in [EF].
Do, 24.11.2011
Gaifman-Normalform; Beginn des Beweises des Satzes von Gaifman
Übungsblatt 5 ausgeteilt.
Material:
Kapitel 5 (bis inkl. Seite 127).
Weitere Lektüre:
Kapitel 2.5 in [EF], Kapitel 4.1-4.3 und in [L].
Di, 29.11.2011
Abschluss des Beweises des Satzes von Gaifman; die Gaifman-Lokalität der Logik erster Stufe
Material:
Kapitel 5 (bis Seite 142).
Weitere Lektüre:
Kapitel 2.5 in [EF], Kapitel 4.1-4.3 und 4.5 in [L].
Do, 01.12.2011
Beweis und Anwendungen der 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
Übungsblatt 6 ausgeteilt.
Material:
Kapitel 5 (bis Seite 157).
Weitere Lektüre:
Kapitel 4 und 6.6 in [L].
Di, 06.12.2011
Anwendungen des Satzes von Seese über das Auswertungsproblem der Logik erster Stufe auf Klassen von Graphen von beschränktem Grad; eine untere Schranke für Formeln in Gaifman-Normalform; Beginn des Beweises des Satzes von McNaughton und Papert
Material:
Kapitel 5 (komplett) und Kapitel 6 (bis Seite 173).
Weitere Lektüre:
Kapitel 7.5 in [L]. Die Originalarbeit mit der unteren Schranke für Formeln in Gaifman-Normalform finden Sie hier; eine Vorabversion ist auch hier erhältlich. Einen Überblick über so genannte Algorithmische Metatheoreme finden Sie hier.
Do, 08.12.2011
Abschluss des Beweises des Satzes von McNaughton und Papert; Beweiskalküle; Sequenzen
Übungsblatt 7 ausgeteilt.
Material:
Kapitel 6 (komplett) und Kapitel 7 (bis Seite 209)
Weitere Lektüre:
Kapitel 7.5 in [L], Kapitel 6.4 in [EF] und Kapitel 4.1 in [EFT].
Di, 13.12.2011
Definition und Korrektheit des Sequenzenkalküls; Formulierung des Vollständigkeitssatzes; Beispiele für Beweise im Sequenzenkalkül; Ableitbare aussagenlogische Sequenzenregeln
Material:
Kapitel 7 (bis Seite 225)
Weitere Lektüre:
Kapitel 4 in [EFT].
Do, 15.12.2011
Weitere ableitbare Sequenzenregeln: Quantorenaustauschregeln, Gleichheitsregeln; Widerspruchsfreiheit; das syntaktische Endlichkeitslemma; der Vollständigkeitssatz; Beweis des Vollständigkeitssatzes unter Verwendung des Erfüllbarkeitslemmas
Übungsblatt 8 ausgeteilt.
Material:
Kapitel 7 (bis Seite 241)
Weitere Lektüre:
Kapitel 4 in [EFT].
Di, 20.12.2011
Terminterpretation und reduzierte Terminterpretation; negationstreue Formelmengen; Formelmengen, die Beispiele enthalten; Beginn des Beweises des Satzes von Henkin
Material:
Kapitel 7 (bis Seite 252)
Weitere Lektüre:
Kapitel 5 in [EFT].
Do, 22.12.2011
Abschluss des Beweises des Satzes von Henkin; Beweis des Erfüllbarkeitslemmas für abzählbare Signaturen; Abschluss des Kapitels über den Vollständigkeitssatz
Übungsblatt 9 ausgeteilt.
Material:
Kapitel 7 (komplett)
Weitere Lektüre:
Kapitel 5 in [EFT]. Ein Beweis des Erfüllbarkeitslemma für überabzählbare Signaturen findet sich in Kapitel 5.3 von [EFT].
Di, 10.01.2012
Der Kompaktheitssatz (Endlichkeitssatz); Axiomatisierbarkeit von Unendlichkeit; Nicht-Axiomatisierbarkeit von Endlichkeit und Graphzusammenhang; der Satz von Löwenheim und Skolem; Nicht-Axiomatisierbarkeit von Überabzählbarkeit
Material:
Kapitel 8 (bis inkl. Seite 276)
Weitere Lektüre:
Kapitel 6 in [EFT].
Do, 12.01.2012
Abschluss von Kapitel 8: Absteigender und aufsteigender Satz von Löwenheim und Skolem; elementare Äquivalenz; Nichtstandardmodelle der Arithmetik; der Satz von Skolem: ein abzählbares Nichtstandardmodell der Arithmetik
Übungsblatt 10 ausgeteilt.
Material:
Kapitel 8 (bis inkl. Seite 286)
Weitere Lektüre:
Kapitel 6 in [EFT].
Di, 17.01.2012
Beginn mit Kapitel 9: Die Grenzen der Berechenbarkeit: Entscheidbarkeit, Semi-Entscheidbarkeit und rekursive Aufzählbarkeit; die rekursive Aufzählbarkeit der allgemeingültigen FO-Formeln; Gödelisierung von FO[σAr]
Material:
Kapitel 9 (bis inkl. Seite 300)
Weitere Lektüre:
Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].
Do, 19.01.2012
Die rekursive Aufzählbarkeit einiger definierbarer Zahlenmengen; FO-Definierbarkeit von Relationen und Funktionen; die Klasse Δ0 aller beschränkten FO[σAr]-Formeln; das Lemma über die β-Funktion
Übungsblatt 11 ausgeteilt.
Material:
Kapitel 9 (bis inkl. Seite 312)
Weitere Lektüre:
Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].
Di, 24.01.2012
Turingmaschinen als formales Berechnungsmodell; die Klasse aller Σ1-Formeln; Beweis der Σ1-Definierbarkeit aller TM-berechenbaren partielle Funktionen und aller TM-rekursiv aufzählbaren Relationen; die Unentscheidbarkeit der Theorie der Standardarithmetik
Übungsblatt 12 ausgeteilt.
Material:
Kapitel 9 (bis inkl. Seite 324)
Weitere Lektüre:
Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].
Do, 26.01.2012
Erfüllbarkeit und Allgemeingültigkeit im Endlichen; der Satz von Trakhtenbrot (Трахтенброт); Folgerungen aus dem Satz von Trakthenbrot; Ordnungsinvarianz.
Übungsblatt 12 ausgeteilt.
Material:
Kapitel 9 (komplett)
Weitere Lektüre:
Kapitel 10 in [EFT]; Kapitel 9.1 sowie 5.1 und 5.2 in [L]; Kapitel 7.2.1 in [EF].
Di, 24.01.2012
Beginn mit Kapitel 10: Gödels Unvollständigkeitssätze: Theorien und Axiomatisierbarkeit; die Minimale Arithmetik; Formulierung von Gödels erstem Unvollständigkeitssatz; der Σ1-Transfersatz.
Material:
Kapitel 10 (Seite 326-337)
Weitere Lektüre:
Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].
Do, 02.02.2012
Repräsentierbarkeit von Relationen und Funktionen; Satz über die Repräsentierbarkeit (in Q) der berechenbaren Funktionen und der entscheidbaren Relationen; der Fixpunktsatz (hier zunächst noch ohne Beweis); der Satz über die Unmöglichkeit der Selbstrepräsentierbarkeit; der Satz von Tarski über die Nichtdefinierbarkeit der Wahrheit; die Unentscheidbarkeit der minimalen Arithmethik
Übungsblatt 13 ausgeteilt.
Material:
Kapitel 10 (Seite 338-357)
Weitere Lektüre:
Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].
Di, 07.02.2012
Beweis des Fixpunktsatzes; die Unentscheidbarkeit der Menge aller allgemeingültigen FO[&sigmaAr]-Sätze; Beweis von Gödels erstem Unvollständigkeitssatz; die Existenz von Gödelsätzen; Anmerkungen zu Hilberts Programm
Material:
Kapitel 10 (Seite 350-368)
Weitere Lektüre:
Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].
Do, 09.02.2012
Konsistenzsatz für T; die Peano-Arithmetik; Gödels zweiter Unvollständigkeitssatz; der Satz von Löb.
Zusammenfassung der in der Vorlesung bzw. Übung behandelten Themen; Hinweise zur Prüfungsvorbereitung; Ausblick auf das Seminar "Logik in der Informatik" im SoSe 2012.
Übungsblatt 14 ausgeteilt.
Material:
Kapitel 10 (komplett)
Weitere Lektüre:
Kapitel 18 in [BBJ] sowie Kapitel 10 in [EFT]. Eine ausführliche Erklärung des im Beweis des Satzes von Löb verwendeten Arguments finden Sie auf den Seiten 235-236 in [BBJ].