Logik in der Informatik

Vorlesung im WS 2011/12

Gehalten von Prof. Dr. Nicole Schweikardt
Betreuung der Übungen durch Dr. Dominik D. Freydenberger

Aktuelles

 Im Logbuch finden Sie nach den Vorlesungen Informationen zum Inhalt der einzelnen Vorlesungsstunden und gelegentlich ergänzende Bemerkungen.

Einführung

Die mathematische Logik beschäftigt sich mit den grundlegenden Eigenschaften von formalen Systemen und Sprachen. Wichtige Themen der Logik in der Informatik sind die Ausdrucksstärke formaler Sprachen und die Grenzen und Möglichkeiten des automatischen Schließens. Anwendungen der Logik finden sich in unterschiedlichen Bereichen der Informatik, beispielsweise Rechnerarchitektur, Softwaretechnik, Programmiersprachen, Datenbanken, künstliche Intelligenz, Komplexitäts- und Berechenbarkeitstheorie. In dieser Vorlesung werden klassische Resultate der mathematischen Logik und deren Anwendungen in verschiedenen Bereichen der Informatik vorgestellt. Themen sind beispielsweise: Ausdrucksstärke und Auswertungskomplexität der Logik erster Stufe (Prädikatenlogik), Ehrenfeucht-Fraïssé Spiele, der Satz von Hanf, der Satz von Gaifman, der Satz von Trakhtenbrot, der Vollständigkeitssatz der Logik erster Stufe, die Gödelschen Unvollständigkeitssätze.

Ziel dieser Veranstaltung ist, grundlegende Resultate der mathematischen Logik sowie deren Anwendungen in der Informatik zu verstehen.

Kürzel laut Studienordnung: B-LI, M-LI.  Creditpoints: 9.  SWS: 4 V, 2 Ü.

Inhalte
  1. Einleitung
  2. Syntax und Semantik der Logik erster Stufe
  3. Normalformen
  4. Die Auswertungskomplexität von FO in endlichen Strukturen
  5. Ehrenfeucht-Fraïssé Spiele
  6. Der Satz von Gaifman
  7. Der Satz von McNaughton und Papert
  8. Der Vollständigkeitssatz
  9. Der Kompaktheitssatz und der Satz von Löwenheim und Skolem
  10. Die Grenzen der Berechenbarkeit
  11. Gödels Unvollständigkeitssätze

Skript

Logbuch

 Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden, die in der Vorlesung verwendeten Folien und gelegentlich ergänzende Bemerkungen.

Termine
ZeitOrtLeitung
Vorlesung Dienstags 14:15-16:00 Magnus-Hörsaal in der Informatik, Robert-Mayer-Str. 11-15 Prof. Dr. Nicole Schweikardt
Vorlesung Donnerstags 14:15-16:00 SR 11, Robert-Mayer-Str. 11-15 Prof. Dr. Nicole Schweikardt
Übung 1 Donnerstags 16:15-18:00 SR 11, Robert-Mayer-Str. 11-15 Dr. Dominik D. Freydenberger

Übungsblätter

Prüfungen bzw. Scheine

Vorsicht:

In der Vorlesung und der Übung werden viele wichtige Dinge (insbesondere Beweise, aber auch einiges andere) an der Tafel erklärt. Diese Dinge sind für die Veranstaltung "Logik in der Informatik" wesentlich und daher auch dann prüfungsrelevant, wenn sie nicht in den hier erhältlichen pdf-Dateien enthalten sind.
Zur Vorbereitung auf eine Prüfung (Modulabschlussprüfung oder Diplom-Prüfung) ist es unbedingt notwendig, das gesamte in den Vorlesungs- und Übungsstunden (mit Folien oder an der Tafel) vermittelte Material durchzuarbeiten.

Modulabschlussprüfung (relevant für Studierende in einem Bachelor- oder Master-Studiengang):

Je nach Anzahl der Teilnehmer/innen eine mündliche Prüfung oder eine 180-minütige Klausur.

Im Lauf des Semesters können Bonuspunkte erworben werden, durch deren Einbringen die Note einer bestandenen Modulabschlussprüfung um eine Teilnote verbessert werden kann (also von 4,0 auf 3,7; von 3,7 auf 3,3; von 3,3 auf 3,0; von 3.0 auf 2,7; von 2,7 auf 2,3; von 2,3 auf 2,0; von 2,0 auf 1,7; von 1,7 auf 1,3; von 1,3 auf 1,0).

In der letzten Übungsstunde vor Weihnachten und in der letzten Übungsstunde des Semesters wird je ein 90-minütiger Test geschrieben.
Voraussetzung für den Erwerb von Bonuspunkten, durch deren Einbringen die Note einer bestandenen Modulabschlussprüfung um eine Teilnote verbessert werden kann, sind:

  1. Bestehen der beiden Tests und
  2. Erreichen von mindestens 50 Prozent aller Übungspunkte (bitte beachten Sie, dass dies insbes. die regelmäßige und aktive Teilnahme an den Übungsstunden erfordert, siehe unten).

Scheinerwerb (relevant für Studierende in einem Diplom- oder Lehramts-Studiengang):

In der letzten Übungsstunde vor Weihnachten und in der letzten Übungsstunde des Semesters wird je ein 90-minütiger Test geschrieben.
Voraussetzung für den Scheinerwerb sind:
  1. Bestehen der beiden Tests und
  2. Erreichen von mindestens 50 Prozent aller Übungspunkte (bitte beachten Sie, dass dies insbes. die regelmäßige und aktive Teilnahme an den Übungsstunden erfordert, siehe unten).

Verbindliche "Spielregeln" zum Erwerb von Übungspunkten:

Übungsblätter werden donnerstags nach der Vorlesung ausgeteilt. Am Donnerstag der darauf folgenden Woche wird das jeweilige Übungsblatt in der Übungsstunde besprochen. Zu Beginn dieser Übungsstunde können alle Teilnehmer in eine Liste eintragen, für welche Aufgaben(teile) sie wie viele Übungspunkte angerechnet bekommen wollen. Während der Übungsstunde werden vom Übungsleiter aus dieser Liste willkürlich einzelne Teilnehmer zum Vorrechnen von Aufgaben(teilen) ausgesucht. Falls sich beim Vorrechnen herausstellen sollte, dass ein Teilnehmer keine sinnvolle Lösung vorweisen kann, obwohl er in der Liste Übungspunkte für diese Aufgabe beansprucht hat, geschieht folgendes:
  1. Tritt diese Situation für den jeweiligen Teilnehmer zum ersten Mal in diesem Semester auf, so werden ihm für das gesamte gerade behandelte Übungsblatt keine Übungspunkte angerechnet.
  2. Tritt diese Situation für den jeweiligen Teilnehmer zum zweiten Mal in diesem Semester auf, so kann er in der Veranstaltung "Logik in der Informatik" im WS 2011/12 keine Übungspunkte erwerben.

Literatur
[S] N. Schweikardt. Skript zur Vorlesung "Logik in der Informatik", Goethe-Universität Frankfurt am Main, 2011. Link
[EFT] H.-D. Ebbinghaus, J. Flum, W. Thomas. Einführung in die Mathematische Logik. 5. Auflage, Spektrum Akademischer Verlag, 2007.
[FG] J. Flum, M. Grohe. Parameterized Complexity Theory. Springer-Verlag, 2006.
[EF] H.-D. Ebbinghaus und J. Flum. Finite Model Theory. Springer-Verlag, 2te Auflage, 1999.
[L] L. Libkin. Elements of Finite Model Theory. Springer-Verlag, 2004.
[G] E. Grädel, P. Kolaitis, L. Libkin, M. Marx, J. Spencer, M. Vardi, Y. Venema und S. Weinstein. Finite Model Theory and Its Applications. Springer-Verlag, 2007.
[KK] M. Kreuzer und S. Kühling. Logik für Informatiker. Pearson Studium, 2006.
[S-Logik] U. Schöning. Logik für Informatiker. Springer, 2000
[HR] M. Huth and M. Ryan. Logic in Computer Science - Modelling and Reasoning About Systems. 2nd Edition, Cambridge University Press, 2004.
[BBJ] G. S. Boolos, J. P. Burgess, R. C. Jeffrey. Computability and Logic. 5th Edition, Cambridge University Press, 2007.
[HHIKVV] J. Y. Halpern, R. Harper, N. Immerman, P. G. Kolaitis, M. Y. Vardi, V. Vianu. On the unusual effectiveness of logic in computer science. The Bulletin of Symbolic Logic. Volume 7, Number 2, June 2001 :  Der Artikel ist online hier verfügbar.
[Gaifman] H. Gaifman. On local and non-local properties. Proceedings of the Herbrand Symposium, Logic Colloqium'81, J.Stearn (editor), pp.105-135. North-Holland Publishing Company, 1982.
[Logicomix] A. Doxiaidis, C.H. Papadimitriou, A. Papadatos, A. Di Donna. Logicomix: An Epic Search for Truth. Bloomsbury USA, 2009 :  Informationen zu diesem Comic sind hier erhältlich.

Links
[LICS] IEEE Symposium on Logic in Computer Science (LICS)
[EACSL] European Association for Computer Science Logic (EACSL)
zuletzt geändert: Thu Feb 9 09:16:10 2012 von Lucas Heimberg