Aktuelles:

An dieser Stelle finden Sie im Laufe des Semesters aktuelle Mitteilungen. Bitte sehen Sie regelmäßig nach, ob es Neues gibt. Die erste Vorlesung fand am Dienstag, den 14.10.2008 von 14:15 Uhr bis 16:00 Uhr im Magnus-Hörsaal, Robert-Mayer-Str. 11-15, statt. Die erste Übungsstunde fand am Dienstag, 21.10.2008 von 16:15 bis 18:00 Uhr im Magnus-Hörsaal 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:

Syntax und Semantik der Logik erster Stufe Strukturen Syntax der Logik erster Stufe Semantik der Logik erster Stufe Das Koinzidenzlemma Das Isomorphielemma Normalformen Äquivalenz und Folgerung Das Substitutionslemma Die pränexe Normalform Termreduzierte Formeln und relationale Signaturen Ehrenfeucht-Fraïssé Spiele Das m-Runden EF-Spiel Der Satz von Ehrenfeucht Logische Reduktionen Der Satz von Hanf Der Satz von Fraïssé Der Satz von Gaifman Formulierung und Beweis des Satzes von Gaifman Die Gaifman-Lokalität der Logik erster Stufe Der Satz von Seese über Klassen von Graphen von beschränktem Grad Eine untere Schranke für Formeln in Gaifman-Normalform Der Satz von McNaughton und Papert Die Berechnungskomplexität der Logik erster Stufe Die Auswertung von Formeln in endlichen Strukturen Der Satz von Trakhtenbrot Der Vollständigkeitssatz Beweiskalküle Ein Sequenzenkalkül Ableitbare Regeln im Sequenzenkalkül Widerspruchsfreiheit und das syntaktische Endlichkeitslemma Der Vollständigkeitssatz Der Kompaktheitssatz und der Satz von Löwenheim und Skolem Der Satz von Löwenheim und Skolem Der Kompaktheitssatz (Endlichkeitssatz) 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: 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 WS08/09 keinen Schein erwerben.

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:

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