Logik (WS 2020/21)
Vergangene VeranstaltungDiese Seite bezieht sich auf eine Vorlesung aus vorherigen Jahren. Aktuelle Termine und Arbeitsmaterialien sind hier zu finden. |
Vorlesungsablauf
Die Vorlesung wird dieses Wintersemester aufgrund der Covid-19-Situation nicht als Präsenzveranstaltung stattfinden, sondern online. Bitte melden Sie sich im Moodle-Kurs an (für die Anmeldung wird ein Passwort benötigt, falls Sie sich noch anmelden wollen, schreiben Sie eine Mail an Herrn Eggert) für alle Materialien und weitere Informationen (werden regelmäßig aktualisiert).
Wir werden wöchentlich Videos von der Vorlesung bereitstellen. Übungsaufgaben werden wie gewohnt online abgegeben und bewertet. Auch die Besprechung der Übungen erfolgt online durch Videos. Eure Fragen zum Stoff können im Moodle-Forum gestellt werden und werden von uns beantwortet.
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 WS19/20 (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:
- 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 + Jar) - Theorembeweiser für die Prädikatenlogik 1. Stufe (basierend auf Resolution):
Otter - PROLOG-Interpreter bzw. -Compiler (zip-Datei mit Prolog-Beispielen)
Termine
Vorlesung und Übung
online als Aufzeichnungen zum Download, ggf. ergänzt durch Fragestunden über BigBlueButton.
Alle Details und Links sind im Moodle zu finden.
Prüfung/Klausur
Die Klausur findet voraussichtlich am ??.??.2021, von ??:??-??:?? Uhr statt.