Logik in der Informatik Prof. Dr. Martin Grohe

Aktuelles

Einführung

Logik beschäftigt sich mit den grundlegenden Eigenschaften von formalen Systemen und Sprachen. Wichtige Themen der Logik in der Informatik sind die Ausdruckstärke formaler Sprachen und die Grenzen und Möglichkeiten des automatischen Schließens. Anwendungen der Logik finden sich in so unterschiedlichen Bereichen der Informatik wie Rechnerarchitektur, Softwaretechnik, Programmiersprachen, Datenbanken, künstliche Intelligenz, Komplexitäts- und Berechenbarkeitstheorie.

Aufbauend auf den Grundlagen der Theoretischen Informatik I werden in dieser Vorlesung auch tiefliegendere Ergebnisse und Zusammenhänge aus der Logik vorgestellt. Dabei wird es sowohl um klassische Sätze der mathematischen Logik, etwa die Gödelschen Unvollständigkeitssätze, als auch um die Anwendungen in verschiedenen Bereichen der Informatik gehen.

Die Vorlesung ist eine Kernveranstaltung im Bereich der Logik in der Informatik, auf der weitere Veranstaltungen an den Lehrstühlen Logik in der Informatik, Logik und Datenbanktheorie sowie Logik und Diskrete Systeme aufbauen.

Inhalt

Das folgende Inhaltsverzeichnis wird im Laufe der Vorlesung noch ergänzt und möglicherweise verändert.

1. Wiederholung: Die Logik der 1.Stufe
2. Der Vollständigkeitssatz
3. Einführung in den interaktiven Theorembeweiser ISABELLE
   Zusätzliche Ressourcen: ersteStufe.thy Einfuehrung.thy EinfuehrungA.thy
4. Grundlagen des automatischen Beweisens
5. Hoare Logik und Softwareverifikation
6. Modallogik
7. Die Ausdrucksstärke der Logik der 1. Stufe
8. Die Gödelschen Unvollständigkeitssätze
9. Die Logik der 2. Stufe

Logbuch

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

Informationen zum Vorlesungsbetrieb

Zeiten und Raum

Dienstags und Donnerstags 13-15 im Schrödinger Zentrum (Rudower Chaussee 26), Raum 1'303

 

Dozent

Prof. Dr. Martin Grohe

Sprechstunde in WS05/06: Dienstags 15:00 - 16:00

Übungen

Ergänzend zu den Vorlesungen finden 2-stündige Übungen statt.

Zeit und Raum

Donnerstags 15-17 im Schrödinger Zentrum (Rudower Chaussee 26), Raum 1'303

 

Übungsleiter

Dipl. Math. Mark Weyer

Übungsaufgaben

Es gibt regelmäßig Übungsaufgaben, deren erfolgreiche Bearbeitung (mindestens 40% der Punkte) Voraussetzung für den Scheinerwerb und die Zulassung zur Prüfung ist.

• Blatt 1 (24.10.2006; Abgabe am 31.10.2006)
• Blatt 2 (31.10.2006; Abgabe am 7.11.2006)
• Präsenzaufgaben und Lösungen für die Übung am 2.11.2006 (Isabelle)
• Blatt 3 (7.11.2006; Abgabe am 21.11.2006)
• Blatt 4 (14.11.2006; Abgabe am 21.11.2006)
• Blatt 5 (21.11.2006; Abgabe am 28.11.2006)
• Blatt 6 (28.11.2006; Abgabe am 5.12.2006)
• Blatt 7 (7.12.2006; Abgabe am 19.12.2006)
• Blatt 8 (19.12.2006; Abgabe am 9.1.2007)
• Blatt 9 (9.1.2007; Abgabe am 16.1.2007)
• Blatt 10 (16.1.2007; Abgabe am 23.1.2007)
• Blatt 11 (23.1.2007; Abgabe am 30.1.2007)
• Blatt 12 (30.1.2007; Abgabe am 6.2.2007)

Prüfung

Zu Beginn der Semesterferien finden mündliche Prüfungen statt. Für die Zulassung zur Prüfung müssen mindestens 40% der Punkte in den Übungsaufgaben erworben werden.

Literatur