Current entry

Logfile: Logik in der Informatik

Lecture  in Winter 2011/12

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


  1. Di, 25.10.2011
  2. 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.
  3. Do, 27.10.2011, 14h15-15h45
  4. 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].
  5. Do, 27.10.2011, 16h15-17h45
  6. 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].
  7. Di, 01.11.2011
  8. 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].
  9. Do, 03.11.2011
  10. 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.
  11. Di, 08.11.2011
  12. 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].
  13. Do, 10.11.2011
  14. 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].
  15. Di, 15.11.2011
  16. 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].
  17. Do, 17.11.2011
  18. 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].
  19. Di, 22.11.2011
  20. 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].
  21. Do, 24.11.2011
  22. 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].
  23. Di, 29.11.2011
  24. 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].
  25. Do, 01.12.2011
  26. 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].
  27. Di, 06.12.2011
  28. 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.
  29. Do, 08.12.2011
  30. 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].
  31. Di, 13.12.2011
  32. 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].
  33. Do, 15.12.2011
  34. 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].
  35. Di, 20.12.2011
  36. 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].
  37. Do, 22.12.2011
  38. 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].
  39. Di, 10.01.2012
  40. 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].
  41. Do, 12.01.2012
  42. 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].
  43. Di, 17.01.2012
  44. 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].
  45. Do, 19.01.2012
  46. 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].
  47. Di, 24.01.2012
  48. 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].
  49. Do, 26.01.2012
  50. 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].
  51. Di, 24.01.2012
  52. 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].
  53. Do, 02.02.2012
  54. 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].
  55. Di, 07.02.2012
  56. 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].
  57. Do, 09.02.2012
  58. 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].