WS 2013/14: Logik

Dozentin:
Prof. Dr. Barbara König (Email)

Übungsleitung:
Dr. Sander Bruggink (Email)

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 SS 2013 (mit den Folien des vorherigen Semesters).

• 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.

Folgende Werkzeuge werden in der Vorlesung eingesetzt:

Aussagenlogik:

• SAT-Solver: Überprüfung der Erfüllbarkeit von aussagenlogischen Formeln
  Limboole
  [Sudoku-Formel für limboole]

Prädikatenlogik:

• Anschauliche Lehrsoftware für die Prädikatenlogik:
  Tarski's World bzw. Tarski's World (Java Applet)
• Theorembeweiser für die Prädikatenlogik 1. Stufe (basierend auf Resolution):
  Otter
• PROLOG-Interpreter bzw. -Compiler:
  • SWI Prolog
  • GNU Prolog

Vorlesung:

• Mittwoch, 8:30–10:00, LB 107
  Erste Vorlesung: 23.10.2013.

Übungsgruppen

• Gruppe 1: Mittwoch, 16:00–18:00, LE 105
• Gruppe 2: Mittwoch, 16:00–18:00, LC 137 (fällt aus!)
• Gruppe 3: Donnerstag, 10:00–12:00, LC 137
• Gruppe 4: Donnerstag, 12:00–14:00, LE 120
• Gruppe 5: Donnerstag, 14:00–16:00, LF 035
• Gruppe 6: Donnerstag, 16:00–18:00, LF 035 (fällt aus!)
• Gruppe 7: Freitag, 8:30–10:00, LF 035
• Gruppe 8: Freitag, 12:00–14:00, LE 120
• Gruppe 9: Freitag, 14:00–16:00, LE 120 (fällt aus!)

Übungsgruppen fangen in der Woche des 6. November an.

• Folien und Übungsblätter
• MOODLE-Seite

Die Logik-Klausur im Sommersemester 2014 findet am Freitag, 1.8.2014, von 8:30-10:30 Uhr im Raum LC 137 statt.

Keine Artikel in dieser Ansicht.