Aktuelles:

An dieser Stelle finden Sie im Laufe des Semesters aktuelle Mitteilungen. Bitte sehen Sie regelmäßig nach, ob es Neues gibt. Die Modulabschlussprüfung wird durch eine mündliche Prüfung abgelegt. Prüfungszeitraum: 02.03.2010, 03.03.2010 und 04.03.2010. Falls Sie eine Modulabschlussprüfung ablegen wollen, vereinbaren Sie bitte mit Frau Nadland (Sekretariat, Raum 116) einen Prüfungstermin und denken Sie daran, das ausgefüllte und unterschriebene Anmeldeformular rechtzeitig im Prüfungsamt abzugeben. Die erste Vorlesung fand am Dienstag, den 13.10.2009 von 14:15 Uhr bis 16:00 Uhr im Magnus-Hörsaal (Robert-Mayer-Str. 11-15) statt. Die erste Übungsstunde findet am Dienstag, den 20.10.2009 von 16:15 Uhr bis 18:00 Uhr im Magnus-Hörsaal (Robert-Mayer-Str. 11-15) statt. Informationen zum Inhalt der einzelnen Vorlesungsstunden und gelegentlich ergänzende Bemerkungen finden Sie (nach den Vorlesungen) im Logbuch.

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:

0. Einleitung (Skript, handschriftlich) 1. Syntax und Semantik der Logik erster Stufe (Skript, handschriftlich)   1.1. Strukturen   1.2. Syntax der Logik erster Stufe   1.3. Semantik der Logik erster Stufe   1.4. Das Koinzidenzlemma   1.5. Das Isomorphielemma 2. Normalformen (handschriftlich)   2.1. Äquivalenz und Folgerung   2.2. Das Substitutionslemma   2.3. Die pränexe Normalform   2.4. Termreduzierte Formeln und relationale Signaturen 3. Die Auswertungskomplexität von FO in endlichen Strukturen (handschriftlich) 4. Ehrenfeucht-Fraïssé Spiele (handschriftlich)   4.1. Das m-Runden EF-Spiel   4.2. Der Satz von Ehrenfeucht   4.3. Logische Reduktionen   4.4. Der Satz von Hanf   4.5. Der Satz von Fraïssé 5. Der Satz von Gaifman (handschriftlich)   5.1. Formulierung und Beweis des Satzes von Gaifman   5.2. Die Gaifman-Lokalität der Logik erster Stufe   5.3. Der Satz von Seese über Klassen von Graphen von beschränktem Grad   5.4. Eine untere Schranke für Formeln in Gaifman-Normalform 6. Der Satz von McNaughton und Papert (handschriftlich) 7. Der Vollständigkeitssatz (handschriftlich)   7.1. Beweiskalküle   7.2. Ein Sequenzenkalkül   7.3. Ableitbare Regeln im Sequenzenkalkül   7.4. Widerspruchsfreiheit und das syntaktische Endlichkeitslemma   7.5. Der Vollständigkeitssatz 8. Der Kompaktheitssatz und der Satz von Löwenheim und Skolem (handschriftlich)   8.1. Der Kompaktheitssatz (Endlichkeitssatz)   8.2. Der Satz von Löwenheim und Skolem   8.3. Elementare Äquivalenz und Nichtstandardmodelle der Arithmetik 9. Die Grenzen der Berechenbarkeit (handschriftlich)   9.1. Entscheidbarkeit und rekursive Aufzählbarkeit   9.2. Gödelisierung von FO[σAr]   9.3. FO-Definierbarkeit der berechenbaren Funktionen   9.4. Der Satz von Trakhtenbrot 10. Gödels Unvollständigkeitssätze (handschriftlich)   10.1. Theorien und Axiomatisierbarkeit   10.2. Die minimale Arithmetik   10.3. Der Fixpunktsatz und die Unentscheidbarkeit der Logik erster Stufe   10.4. Gödels erster Unvollständigkeitssatz   10.5. Gödels zweiter Unvollständigkeitssatz Begleitend zur Vorlesung wird ein Vorlesungsskript erstellt, das nach und nach hier erhältlich sein wird: Einleitung und Kapitel 1.

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. Blatt 1 (ausgeteilt am Di, 20.10.2009; zu bearbeiten bis Di, 27.10.2009) Blatt 2 (ausgeteilt am Di, 27.10.2009; zu bearbeiten bis Di, 03.11.2009) Blatt 3 (ausgeteilt am Di, 03.11.2009; zu bearbeiten bis Di, 10.11.2009) Blatt 4 (ausgeteilt am Di, 10.11.2009; zu bearbeiten bis Di, 17.11.2009) Blatt 5 (ausgeteilt am Di, 17.11.2009; zu bearbeiten bis Di, 24.11.2009) Blatt 6 (ausgeteilt am Di, 24.11.2009; zu bearbeiten bis Di, 01.12.2009) Blatt 7 (ausgeteilt am Di, 01.12.2009; zu bearbeiten bis Di, 08.12.2009) Blatt 8 (ausgeteilt am Di, 08.12.2009; zu bearbeiten bis Di, 15.12.2009) Blatt 9 (ausgeteilt am Di, 15.12.2009; zu bearbeiten bis Di, 12.01.2010) Blatt 10 (ausgeteilt am Di, 12.01.2010; zu bearbeiten bis Di, 19.01.2010) Blatt 11 (ausgeteilt am Di, 19.01.2010; zu bearbeiten bis Di, 26.01.2010) Blatt 12 (ausgeteilt am Di, 26.01.2010; zu bearbeiten bis Di, 02.02.2010) Blatt 13 (ausgeteilt am Di, 02.02.2010; zu bearbeiten bis Di, 09.02.2010)

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: 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 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.

Literatur:

[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] 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 Colloquium'81, J. Stearn (editor), pp. 105-135. North-Holland Publishing Company, 1982.

Links:

• IEEE Symposium on Logic in Computer Science (LICS)
• European Association for Computer Science Logic (EACSL)