Dozentin: Prof. Dr. Barbara König (barbara_koenig@uni-due.de)

Übungsleitung: Tobias Heindel

Aktuelle Ankündigungen:

Im WS 09/10 wird die Klausur für Logik am 22.2. von 10 bis 12 Uhr in LB 131 stattfinden.

Falls Sie in Logik eine mündliche Fachprüfung machen wollen, dann lesen Sie bitte folgende Webseite.

Klausur

Die vorläufigen Klausurergebnisse kann man hier abrufen. Die Noten beinhalten bereits die Bonuspunkte aus den Übungen. Die Klausureinsicht findet am Freitag, den 18.9., von 10-11 Uhr im Raum LF 261 statt.

Einsichtstermin
für die Klausur vom 23. Februar:
26. März 2010
15:30 Uhr
Raum: LF 261 (Gebäude LF, Campus Duisburg)


Die Klausur findet am 07.08.2009 statt, und zwar von 14.00 Uhr bis 16.00 Uhr in Raum MD 162.

Alte Klausuraufgaben: Eine Sammlung alter Klausuraufgaben kann man hier herunterladen. In der Klausur werden ca. sechs Aufgaben ähnlicher Schwierigkeit gestellt werden.

Kurzbeschreibung

Die Logik ist eine Grundlagendisziplin der Informatik. Die klassischen Fragestellungen der Logik sind „Was ist eine wahre Aussage?“, „Was ist ein Modell einer Aussage?“ oder „Was kann man allein durch Axiome beschreiben?“. Es gibt aber auch eine Liste von Anwendungen der Logik: hier dient Logik als Spezifikations- oder Programmiersprache (z.B. PROLOG). Weitere Anwendugsgebiete sind der Schaltkreisentwurf, Datenbank-Anfragesprachen, Programm-Verifikation und automatisches Beweisen. Schließlich sollte man auf die strikte Trennung zwischen Syntax und Semantik hinweisen, die in der Logik wenigstens seit Tarski vorgenommen wird (aber bei Programmiersprachen nicht immer so ganz klar ist), und wohl nirgends anders in der Informatik deutlicher zu Tage tritt.

Siehe auch die Webseite aus dem WS 07/08 (mit den Folien des Vorjahres).

Termine

Vorlesung

• Mi, 12–14, LE 105

Vorlesungsbeginn: Mittwoch, 15. April

Übungsgruppen

• Gruppe 1, Mi, 14.15–15.15, LC 137
• Gruppe 2, Fr, 12.15–13.15, LC 137

Tutorium

• Do, 14–16 (Raum LE 105)

Folien

Die Folien werden ähnlich zu den Folien im Wintersemester 07/08 sein. Sie sind von der Webseite der letztjährigen Vorlesung erhältlich.

Hinweis: s/w = schwarz-weiß

• Alle Folien (Stand: 22.07.09): [1x1] [2x2] [1x1 (s/w)] [2x2 (s/w)]

Folien, unterteilt in Kapitel

Organisatorisches und Einführung

• Organisation (Stand: 06.05.09) [1x1] [2x2] [1x1 (s/w)] [2x2 (s/w)]
• Einführung (Stand: 15.04.09) [1x1] [2x2] [1x1 (s/w)] [2x2 (s/w)]

Aussagenlogik

• Grundbegriffe, Äquivalenz und Normalformen (Stand: 06.05.09) [1x1] [2x2] [1x1 (s/w)] [2x2 (s/w)]
• Resolution (Stand: 20.05.09) [1x1] [2x2] [1x1 (s/w)] [2x2 (s/w)]

Prädikatenlogik

• Grundbegriffe, Äquivalenz und Normalformen (Stand: 17.06.09) [1x1] [2x2] [1x1 (s/w)] [2x2 (s/w)]
• Herbrandtheorie und Resolution (Stand: 22.07.09) [1x1] [2x2] [1x1 (s/w)] [2x2 (s/w)]
• Grundlagen der Logik-Programmierung und Ausblick (Stand: 22.07.09) [1x1] [2x2] [1x1 (s/w)] [2x2 (s/w)]

Übungblätter

• Blatt 1 [pdf] – Abgabetermin: Mo, 20.04. 12:00.
• Blatt 2 [pdf] – Abgabetermin: Mo, 27.04. 12:00.
• Blatt 3 [pdf] – Abgabetermin: Mo, 04.05. 12:00.
• Blatt 4 [pdf] – Abgabetermin: Mo, 11.05. 12:00.
• Blatt 5 [pdf] – Abgabetermin: Mo, 18.05. 12:00.
• Blatt 6 [pdf] – Abgabetermin: Mo, 25.05. 12:00.
  Achtung Es hat sich ein kleiner Fehler eingeschlichen, und zwar bei Aufgabe 2.
  Bitte F durch F' ersetzen.
  Blatt 6 (korrigiert) [pdf]
• Blatt 7 [pdf] – Abgabetermin: Mi, 03.06., 12:00.
• Blatt 8 [pdf] – Abgabetermin: Mo, 08.06. 12:00.
• Blatt 9 [pdf] – Abgabetermin: Mo, 15.06. 12:00.
• Blatt 10 [pdf] – Abgabetermin: Mo, 22.06. 12:00.
• Blatt 11 [pdf] – Abgabetermin: Mo, 29.06. 12:00.
• Blatt 12 [pdf] – Abgabetermin: Mo, 06.07. 12:00.
• Blatt 13 [pdf] – Abgabetermin: Mo, 13.07. 12:00.
• Blatt 14 [pdf] – Abgabetermin: Mo, 20.07. 12:00.

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
• Theorembeweiser für die Prädikatenlogik 1. Stufe (basierend auf Resolution):
  Otter
• PROLOG-Interpreter bzw. -Compiler:
  • SWI Prolog
  • GNU Prolog