Der Webauftritt der Arbeitsgruppe Theorie komplexer Systeme ist umgezogen. Werden Sie nicht automatisch weitergeleitet, nutzen Sie bitte folgenden Link:

http://www.tks.informatik.uni-frankfurt.de/

Theorie komplexer Systeme
Prof. Dr. Nicole Schweikardt
Institut für Informatik
Johann Wolfgang Goethe-Universität
Frankfurt am Main

Logik in der Informatik
Wintersemester 2009/2010

Eintrag im LSF: Vorlesung, Übung

Aktuelles   Einführung   Inhalt   Logbuch   Vorlesung&Übung   Übungsaufgaben   Scheinerwerb/Modulabschlussprüfung    Literatur    Links   

Aktuelles:
An dieser Stelle finden Sie im Laufe des Semesters aktuelle Mitteilungen. Bitte sehen Sie regelmäßig nach, ob es Neues gibt.

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: Aussagenlogik, Resolution, 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.

Inhalt:
  1. Einleitung
  2. Syntax und Semantik der Logik erster Stufe
    1. Strukturen
    2. Syntax der Logik erster Stufe
    3. Semantik der Logik erster Stufe
    4. Das Koinzidenzlemma
    5. Das Isomorphielemma
  3. Normalformen
    1. Äquivalenz und Folgerung
    2. Das Substitutionslemma
    3. Die pränexe Normalform
    4. Termreduzierte Formeln und relationale Signaturen
  4. Die Auswertungskomplexität von FO in endlichen Strukturen
  5. Ehrenfeucht-Fraïssé Spiele
    1. Das m-Runden EF-Spiel
    2. Der Satz von Ehrenfeucht
    3. Logische Reduktionen
    4. Der Satz von Hanf
    5. Der Satz von Fraïssé
  6. Der Satz von Gaifman
    1. Formulierung und Beweis des Satzes von Gaifman
    2. Die Gaifman-Lokalität der Logik erster Stufe
    3. Der Satz von Seese über Klassen von Graphen von beschränktem Grad
    4. Eine untere Schranke für Formeln in Gaifman-Normalform
  7. Der Satz von McNaughton und Papert
  8. Der Satz von Trakhtenbrot
  9. Der Vollständigkeitssatz
    1. Beweiskalküle
    2. Ein Sequenzenkalkül
    3. Ableitbare Regeln im Sequenzenkalkül
    4. Widerspruchsfreiheit und das syntaktische Endlichkeitslemma
    5. Der Vollständigkeitssatz
  10. Der Kompaktheitssatz und der Satz von Löwenheim und Skolem
    1. Der Satz von Löwenheim und Skolem
    2. Der Kompaktheitssatz (Endlichkeitssatz)
  11. Die Gödelschen Unvollständigkeitssätze

Begleitend zur Vorlesung wird ein Vorlesungsskript erstellt, das nach und nach hier erhältlich sein wird.

Logbuch:
Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden und gelegentlich ergänzende Bemerkungen

Informationen zum Vorlesungs- und Übungsbetrieb:
Vorlesung:
Dienstags von 14:15-16:00 Uhr und Donnerstags von 16:15-18:00 Uhr im Magnus-Hörsaal (Robert-Mayer-Str. 11-15)
 
Dozentin:   Prof. Dr. Nicole Schweikardt   (Sprechstunde im WS09/10: Mittwochs 15-16 Uhr, Raum 115)
 
Übung:
Dienstags von 16:15-18:00 Uhr im Magnus-Hörsaal (Robert-Mayer-Str. 11-15)
 
Leitung:   Dipl.-Inf. André Hernich   (Sprechstunde im WS09/10: Donnerstag 15-16 Uhr, Raum 113)
 

Übungsaufgaben:
Es wird regelmäßig Übungsaufgaben geben, deren erfolgreiche Bearbeitung Voraussetzung für den Scheinerwerb ist.

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

In der letzten Übungsstunde vor Weihnachten (d.h. am 15.12.2009) und in der letzen Übungsstunde des Semesters (d.h. am 09.02.2010) wird ein 90-minütiger Test geschrieben. Voraussetzung für den Scheinerwerb sind: (1) Bestehen der beiden Tests, (2) regelmäßige aktive Teilnahme an den Übungen und (3) Erreichen von mindestens 40% aller Übungspunkte.

Verbindliche "Spielregeln" zum Erwerb von Übungspunkten:
Übungsblätter werden dienstags nach der Vorlesung ausgeteilt. Am darauf folgenden Dienstag 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 Ü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 Sitation für den jeweiligen Teilnehmer zum zweiten Mal in diesem Semester auf, so kann er in der Veranstaltung "Logik in der Informatik" im WS09/10 keinen Schein erwerben.

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

Je nach Teilnehmerzahl eine mündliche Prüfung oder eine 180-minütige Klausur.

Literatur:
[EFT] H.-D. Ebbinghaus, J. Flum, W. Thomas, Einführung in die Mathematische Logik. 5. Auflage, Spektrum Akademischer Verlag, 2007.
[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] 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.

Links:

 

Last modified: Tue Sep 15 16:20:00 CEST 2009
Nicole Schweikardt