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

Logik in der Informatik
Wintersemester 2008/2009

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. 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
  2. Normalformen
    1. Äquivalenz und Folgerung
    2. Das Substitutionslemma
    3. Die pränexe Normalform
    4. Termreduzierte Formeln und relationale Signaturen
  3. 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é
  4. 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
  5. Der Satz von McNaughton und Papert
  6. Die Berechnungskomplexität der Logik erster Stufe
    1. Die Auswertung von Formeln in endlichen Strukturen
    2. Der Satz von Trakhtenbrot
  7. 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
  8. Der Kompaktheitssatz und der Satz von Löwenheim und Skolem
      Der Satz von Löwenheim und Skolem
      Der Kompaktheitssatz (Endlichkeitssatz)
  9. Die Gödelschen Unvollständigkeitssätze

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
 
Übung:
Dienstags 16:15-18:00 Uhr im Magnus Hörsaal, Robert-Mayer-Str. 11-15.
 
Dozentin:
Prof. Dr. Nicole Schweikardt (Sprechstunde im WS08/09: Mittwochs 15-16 Uhr, Raum 115)
 
Anmeldung für die Übung:
Über HIS-LSF kann man sich bis spätestens 24. Oktober, 12:00 Uhr anmelden.

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

  • Blatt 1 (ausgeteilt am Di, 21.10.2008; zu bearbeiten bis Di, 28.10.2008)
  • Blatt 2 (ausgeteilt am Di, 28.10.2008; zu bearbeiten bis Di, 04.11.2008)
  • Blatt 3 (ausgeteilt am Di, 04.11.2008; zu bearbeiten bis Di, 11.11.2008)
  • Blatt 4 (ausgeteilt am Di, 11.11.2008; zu bearbeiten bis Di, 18.11.2008)
  • Blatt 5 (ausgeteilt am Di, 18.11.2008; zu bearbeiten bis Di, 25.11.2008)
  • Blatt 6 (ausgeteilt am Di, 25.11.2008; zu bearbeiten bis Di, 02.12.2008)
  • Blatt 7 (ausgeteilt am Di, 02.12.2008; zu bearbeiten bis Di, 09.12.2008)
  • Blatt 8 (ausgeteilt am Di, 09.12.2008; zu bearbeiten bis Di, 16.12.2008)
  • Blatt 9 (online gestellt am Mo, 22.12.2008; zu bearbeiten bis Di, 13.01.2009)
  • Blatt 10 (ausgeteilt am Di, 13.01.2009; zu bearbeiten bis Di, 20.01.2009)
  • Blatt 11 (online gestellt am Di, 20.01.2009; zu bearbeiten bis Di, 27.01.2009)
  • Blatt 12 (ausgeteilt am Di, 27.01.2009; zu bearbeiten bis Di, 03.02.2009)
  • Blatt 13 (ausgeteilt am Di, 03.02.2009; zu bearbeiten bis Di, 10.02.2009)

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

Alte Version:
In der letzten Übungsstunde vor Weihnachten (d.h. am 16.12.2008) und in der letzen Übungsstunde des Semesters (d.h. am 10.02.2009) 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.

Neue Version: Die 90-minütigen Tests entfallen.
Somit gelten folgende Voraussetzungen für den Scheinerwerb:
(1) regelmäßige aktive Teilnahme an den Übungen und (2) 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 von der Dozentin 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 WS08/09 keinen Schein erwerben.

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

Die Modulabschlussprüfung wird durch eine mündliche Prüfung abgelegt. Prüfungszeitraum: 24.03.2009, 25.03.2009 und 26.03.2009.
Falls Sie eine Modulabschlussprüfung ablegen wollen, vereinbaren Sie bitte mit Frau Nadland (Sekretariat, Raum 116) einen Prüfungstermin (für den 24.03.2009, den 25.03.2009 oder den 26.03.2009) und denken Sie daran, das ausgefüllte und unterschriebene Anmeldeformular rechtzeitig im Prüfungsamt abzugeben.

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.

Links:

 

Last modified: Wed Dec 17 13:28:03 CET 2008
Nicole Schweikardt