Logik (WS 2019/20)

Dozentin
Prof. Dr. Barbara König

Übungsleitung
Richard Eggert

Inhalt und Lernziele

Logik dient in der Informatik unter anderem als Grundlage der Datenbanken (Abfragesprache SQL), als Beschreibungssprache für Schaltkreise und als Modellierungs- und Spezifikationssprache, wo sie auch für die Analyse und Verifikation von Programmen eingesetzt wird. In Form der Logik-Programmiersprache Prolog wird Logik auch zur Wissensverarbeitung und für Expertensysteme eingesetzt. Außerdem ist die Logik ein Anwendungsgebiet der Informatik, beispielsweise bei der Entwicklung von Theorembeweisern. Im Rahmen dieser Veranstaltung werden die Grundlagen der Aussagen- und Prädikatenlogik und ihre Anwendungen vermittelt. Inhalte im Einzelnen:

  • Aussagenlogik (Grundbegriffe, Äquivalenz und Normalformen, Hornformeln, Resolution in der Aussagenlogik, Anwendung SAT-Solver)
  • Prädikatenlogik erster Stufe (Grundbegriffe, Normalformen, Unentscheidbarkeit der Prädikatenlogik, Herbrandtheorie, Resolution in der Prädikatenlogik)
  • Grundlagen der Logik-Programmierung (SLD-Resolution)

Siehe auch die Webseite aus dem WS18/19 (mit den Folien des vorigen Semesters).

Literatur

  • Die Vorlesung stützt sich im wesentlichen auf: Uwe Schöning, Logik für Informatiker. Spektrum, 2000.
  • Ein sehr gutes englisches Einführungsbuch ist Language, proof, and logic, das es auch in deutscher Übersetzung gibt:
    John Barwise, John Etchemendy, Sprache, Beweis und Logik. Mentis, 2005
  • Kreuzer, Kühling, Logik für Informatiker. Pearson, 2006
  • Tjark Weber, A SAT-based Sudoku Solver. LPAR 2005.

Tools

Folgende Werkzeuge werden in der Vorlesung eingesetzt:

Aussagenlogik:

Prädikatenlogik:

Termine

Vorlesung

  • Mittwoch, 8:30-10:00, LB 107
  • Erste Vorlesung am 16.10.2019

Übungsgruppen

  • Gruppe 1: Mi, 16–18, LE 105
    (Tutor: Shiyam Sivam)
  • Gruppe 2: Do, 10–12, LK 051
    (Tutor: Annika Johannimloh)
  • Gruppe 3: Do, 10–12, LE 120
    (Tutor: Jeannine Veseljak)
  • Gruppe 4: Do, 12–14, LE 120
    (Tutor: Matthias Schaffeld)
  • Gruppe 5: Do, 16–18, LE 120
    (Tutor: Richard Eggert)
  • Gruppe 6: Fr, 12–14, LE 120
    (Tutor: Yaman Lahdo)

Die Übungsgruppen beginnen ab dem 30.10.2019.

Prüfung/Klausur

Die Klausur findet voraussichtlich am Donnerstag, den 20. Februar 2020, von 15:30-17:30 Uhr statt.

Nachschreibeklausur

Die Klausur findet Donnerstag, den 27. August 2020, von 15:30-17:30 Uhr in den Räumen LX 1205 und LX 1203 statt. Weitere Informationen, wie die Sitzplatzliste, werden per Moodle bekanntgegeben.

Links