Logbuch

Hier finden Sie Informationen zum Verlauf der Vorlesung

  1. Montag, 13.10.08
    Kapitel 1: Übersicht über die Vorlesung, Organisatorisches
  2. Montag, 20.10.08
    Kapitel 2 (bis Folie 24): Gründe für die Verwendung formaler Logik, Syntax und Sematik der Aussagenlogik, Modellierung mit Aussagenlogik (Beispiele)
  3. Montag, 27.10.08
    Kapitel 2: Äquivalenzen und Normalformen
    Kapitel 3 (bis Folie 8): Klauseln und Resolventen
  4. Montag, 3.11.08
    Kapitel 3 (bis Folie 26): Resolution, Resolutionssatz,Erfüllbarkeitstest für AL, Minesweeper-Beispiel
  5. Montag, 10.11.08
    Kapitel 3 (alles außer Folien 37-39): Minesweeper-Beispiel, Hornformeln, Markierungsalgorithmus, Endlichkeitssatz der Aussagenlogik
  6. Montag, 17.11.08
    Kapitel 3 fertig: Königs Lemma, Vollständigkeitssatz
    Kapitel 4 (bis Folie 14): Modallogik: Beispiele, Syntax & Semantik, Äquivalenzen
  7. Montag, 24.11.08
    Kapitel 4 fertig (außer Folien 29-32): Bisimulationen, Baummodelleigenschaft, Algorithmen, Rahmen
    Kapitel 5 (bis Folie 7): Tableaukalkül der Aussagenlogik
  8. Montag, 1.12. 08
    Kapitel 5 fertig: Korrektheit und Vollständigkeit des AL-Tableaukalküls, ML-Tableaukalkül, Selbsttest
  9. Montag, 8.12.08
    Kapitel 4 Nachtrag: Algorithmus für Bisimulationen, Bisimulationen als Spiel
    Kapitel 6 (bis Folie 24): Relationen, Funktionen, Strukturen, Syntax der Prädikatenlogik, viele Beispiele
  10. Montag, 15.12.08
    Kapitel 6 (bis Folie 45): Semantik der Prädikatenlogik, Folien Erstellen, Folien Verstehen, Substitutionen, Äquivalenzen
  11. Montag, 5.1.09
    Kapitel 6 fertig: Normalformen (reduierte Form, NNF, Pränexform, Skolemform)
    Kapitel 7 (bis Folie 11): ProLog und Erfüllbarkeit von PL-Formeln, Herbrand-Strukturen
  12. Montag, 12.1.09
    Kapitel 7 (bis Folie 29): Satz von Löwenheim-Skolem, Grundresolution, PL-Resolution (Vorüberlegungen), Unifikation
  13. Montag, 19.1.09
    Kapitel 7 (bis Folie 48): Unifikationsalgorithmus, PL-Resolutionslemma, Lifting-Lemma, PL-Resolutionssatz, Prologauswertung als Anwendung der PL-Resolution (Beispiele)
  14. Montag, 26.1.09
    Kapitel 7 fertig: Einschränkungen der Resolution, insbesondere SLD-Resolution, Auswertungsstrategien von Prolog
    Kapitel 8 (bis Folie 5): Gödelscher Vollständigkeitssatz, Hilbertkalkül
  15. Montag, 2.2.09
    Kapitel 8 fertig: Sequenzenkalkül, Algorithmische Auswertung von PL-Formeln, Unentscheidbarkeit des Erfüllbarkeitsproblems der Prädikatenlogik, Axiomensysteme und Theorien, Unvollständigkeitssätze