Logik in der Informatik - Einführung in die formale Logik

Vorlesung im WS 2013/14

Gehalten von Prof. Dr. Nicole Schweikardt
Betreuung der Übungen durch M.Sc. Frederik Harwath, Jens Keppeler

Aktuelles

Im Logbuch finden Sie nach den Vorlesungen Informationen zum Inhalt der einzelnen Vorlesungsstunden und gelegentlich ergänzende Bemerkungen.

• Terminänderung:
  Am Donnerstag, den 23.01.14 wird an Stelle der Vorlesungsstunde von 14-16 Uhr eine zusätzliche Übungsstunde stattfinden.
  Als Ausgleich dafür wird am Donnerstag, den 30.01.14 an Stelle der Übung von 16-18 Uhr eine Vorlesungsstunde stattfinden.
• Am Donnerstag, den 19.12.13 wurde zwischen 14 und 16 Uhr ein zum Sammeln von Bonuspunkten notwendiger Test geschrieben.
• Terminänderung:
  Am Donnerstag, den 28.11.13 und am Donnerstag, den 12.12.13 wird an Stelle der Übungsstunde von 16-18 Uhr eine Vorlesungsstunde stattfinden.
  Als Ausgleich dafür wird am Dienstag, den 17.12.13 und am Donnerstag, den 19.12.13 an Stelle der Vorlesung von 14-16 Uhr eine Übungsstunde stattfinden.
• Die ersten drei Vorlesungstermine fanden in der ersten Semesterwoche statt: am Dienstag, den 15.10.2013 von 14:15 Uhr bis 16:00 Uhr im Magnus-Hörsaal, am Donnerstag, den 17.10.2013 von 14:15 bis 16:00 Uhr im Magnus-Hörsaal und am Donnerstag, den 17.10.2013 von 16:15 bis 18:00 Uhr im Magnus-Hörsaal (jeweils in der Robert-Mayer-Str. 11-15).
• Die erste Übungsstunde fand in der zweiten Semesterwoche am Donnerstag, den 24.10.2013 von 16:15 bis 18:00 Uhr im Magnus-Hörsaal (Robert-Mayer-Str. 11-15) statt.

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

Kürzel laut Studienordnung: B-LI, M-LI.  Creditpoints: 9.  SWS: 4 V, 2 Ü.

Inhalte

0. Einleitung
1. Syntax und Semantik der Logik erster Stufe
2. Normalformen
3. Die Auswertungskomplexität von FO in endlichen Strukturen
4. Ehrenfeucht-Fraïssé Spiele
5. Der Satz von Gaifman
6. Der Satz von McNaughton und Papert
7. Der Vollständigkeitssatz
8. Der Kompaktheitssatz und der Satz von Löwenheim und Skolem
9. Die Grenzen der Berechenbarkeit
10. Gödels Unvollständigkeitssätze

Skript

• N. Schweikardt. Skript zur Vorlesung "Logik in der Informatik", Goethe-Universität Frankfurt am Main, 2011.

Logbuch

Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden, die in der Vorlesung verwendeten Folien und gelegentlich ergänzende Bemerkungen.

E-Lectures

Im WS 2013/14 werden Teile der Vorlesungen von studiumdigitale, der E-Learning-Einrichtung der Goethe-Universität, auf Video aufgezeichnet. Die einzelnen Aufzeichnungen finden Sie hier:

• Vorlesung 01: Kapitel 0: Einführung ins Thema; Organisatorisches; Kapitel 1: Signaturen, Strukturen, Isomorphismen [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 15.10.2013)
• Vorlesung 02: Kapitel 1: Isomorphismen; Syntax und Semantik der Logik erster Stufe - bis inkl. Definition 1.23 (Belegungen und Interpretationen) [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 17.10.2013)
• Vorlesung 03: Kapitel 1: Semantik der Logik erster Stufe; Koinzidenzlemma; Isomorphielemma; einführendes Beispiel zu Substitutionen (Diese Vorlesung wurde nicht aufgezeichnet)
• Vorlesung 04: Kapitel 1: Substitutionen und Substitutionslemma; Kapitel 2: Äquivalenz und Folgerung; pränexe Normalform [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 22.10.2013)
• Vorlesung 05: Kapitel 2: pränexe Normalform; termreduzierte Formeln; relationale Signaturen; Kapitel 3: die Breite einer Formel [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 24.10.2013)
• Vorlesung 06: Kapitel 3: die Auswertungskomplexität von FO in endlichen Strukturen; Kapitel 4: Spielregeln des Ehrenfeucht-Fraisse Spiels; Beispiele [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 29.10.2013)
• Vorlesung 07: Kapitel 4: Das EF-Spiel auf zwei linearen Ordnungen [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 31.10.2013)
• Vorlesung 08: Kapitel 4: Der Satz von Ehrenfeucht; Methode zum Nachweis, dass bestimmte Klassen von Strukturen nicht FO-definierbar sind [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 05.11.2013)
• Vorlesung 09: Kapitel 4: Gewinnstrategien für Spoiler; logische Reduktionen; Nachweis, dass Graph-Zusammenhang und Erreichbarkeit nicht FO-definierbar sind; Vorarbeiten zum Satz von Hanf [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 07.11.2013)
• Vorlesung 10: Kapitel 4: Der Satz von Hanf [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 12.11.2013)
• Vorlesung 11: Kapitel 4: Die Hanf-Lokalität der Logik erster Stufe; Hin- und Her-Systeme und der Satz von Fraisse (Aufzeichnung vom 14.11.2013 - steht leider nicht zur Verfügung)
• Vorlesung 12: Kapitel 5: Gaifman-Normalform und der Satz von Gaifman [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 19.11.2013)
• Vorlesung 13: Kapitel 5: Beweis des Satzes von Gaifman [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 21.11.2013)
• Vorlesung 14: Kapitel 5: Die Gaifman-Lokalität der Logik erster Stufe; der Satz von Seese zur Auswertung von FO-Sätzen auf Klassen von Strukturen von beschränktem Grad [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 26.11.2013)
• Vorlesung 15: Kapitel 5: Beweis (und Anwendung) des Satzes von Seese zur Auswertung von FO-Sätzen auf Klassen von Strukturen von beschränktem Grad. Kapitel 6: Vorarbeiten zum Satz von McNaughton und Papert [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 28.11.2013)
• Vorlesung 16: Kapitel 6: Beweis des Satzes von McNaughton und Papert [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 28.11.2013)
• Vorlesung 17: Kapitel 7: Beweiskalküle, Sequenzenkalkül und Formulierung des Vollständigkeitssatzes [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 03.12.2013)
• Vorlesung 18: Kapitel 7: Ableitbare Sequenzenregeln; Widerspruchsfreiheit; das syntaktische Endlichkeitslemma; der Vollständigkeitssatz; Beweis des Vollständigkeitssatzes unter Verwendung des Erfüllbarkeitslemmas [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 05.12.2013)
• Vorlesung 19: Kapitel 7: Terminterpretation und reduzierte Terminterpretation; negationstreue Formelmengen; Formelmengen, die Beispiele enthalten; der Satz von Henkin [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 10.12.2013)
• Vorlesung 20: Kapitel 7: Beweis des Erfüllbarkeitslemmas für abzählbare Signaturen. Kapitel 8: der Kompaktheitssatz (Endlichkeitssatz), Modellklassen und Axiomatisierbarkeit; Axiomatisierbarkeit der Unendlichkeit; Nicht-Axiomatisierbarkeit der Endlichkeit [Flash | QuickTime | Mobile | MP3] und [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 12.12.2013 - aufgrund einer technischen Störung wurden ca. 15 Minuten in der Mitte der Vorlesung nicht aufgezeichnet)
• Vorlesung 21: Kapitel 8: Nicht-Axiomatisierbarkeit von Graphzusammenhang; der Satz von Löwenheim und Skolem; Nicht-Axiomatisierbarkeit von Überabzählbarkeit; Theorien und elementare Äquivalenz; Existenz von Nichtstandardmodellen der Arithmetik [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 12.12.2013)
• Vorlesung 22: Kapitel 8: Ein Nichtstandardmodell der natürlichen Zahlen mit linearer Ordnung; alternativer Beweis (Martin Otto, 2011) dafür, dass endliche lineare Ordnungen gerader Kardinalität nicht FO-definierbar sind in der Klasse aller endlichen linearen Ordnungen; der Satz von Skolem: ein abzählbares Nichtstandardmodell der Arithmetik (Aufzeichnung vom 14.01.2014 - steht leider nicht zur Verfügung)
• Vorlesung 23: Kapitel 9: Entscheidbarkeit, Semi-Entscheidbarkeit und rekursive Aufzählbarkeit; Vereinbarung zur Kodierung der Syntax von FO-Formeln [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 16.01.2014)
• Vorlesung 24: Kapitel 9: Die rekursive Aufzählbarkeit der allgemeingültigen FO-Formeln; Gödelisierung von FO[σ_Ar]; die rekursive Aufzählbarkeit einiger definierbarer Zahlenmengen [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 21.01.2014)
• Vorlesung 25: Kapitel 9: FO-Definierbarkeit von Relationen und Funktionen; die Klasse Δ₀ aller beschränkten FO[σ_Ar]-Formeln; das Lemma über die β-Funktion. [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 28.01.2014)
• Vorlesung 26: Kapitel 9: Turingmaschinen als formales Berechnungsmodell, die Klasse aller Σ₁-Formeln, Beweis der Σ₁-Definierbarkeit aller TM-berechenbaren partielle Funktionen und aller TM-rekursiv aufzählbaren Relationen. [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 30.01.2014)
• Vorlesung 27: Kapitel 9: Die Unentscheidbarkeit der Theorie der Standardarithmetik, der Satz von Trakhtenbrot und die Folgerung, dass die im Endlichen allgemeingültigen FO-Sätze nicht rekursiv aufzählbar sind. [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 30.01.2014)
• Vorlesung 28: Kapitel 9: weitere Folgerung aus dem Satz von Trakthenbrot: die im Endlichen ordnungsinvarianten FO-Sätze sind nicht rekursiv aufzählbar. Kapitel 10: Theorien und Axiomatisierbarkeit; die Minimale Arithmetik Q; Formulierung von Gödels erstem Unvollständigkeitssatz; der Σ₁-Transfersatz [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 04.02.2014)
• Vorlesung 29: Kapitel 10: Abschluss des Beweises des Σ₁-Transfersatzes (d.h. Beweis von Lemma 10.8); Satz über die Repräsentierbarkeit (in der minimalen Arithmetik Q) der berechenbaren totalen Funktionen und der entscheidbaren Relationen. [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 06.02.2014)
• Vorlesung 30: Kapitel 10: Der Fixpunktsatz; der Satz über die Unmöglichkeit der Selbstrepräsentierbarkeit; der Satz von Tarski über die Nichtdefinierbarkeit der Wahrheit; die Unentscheidbarkeit der minimalen Arithmethik; die Unentscheidbarkeit des Allgemeingültigkeitsproblems für FO[σ_Ar]; Beweis von Gödels erstem Unvollständigkeitssatz. (Aufzeichnung vom 11.02.2014 - steht leider nicht zur Verfügung)
• Vorlesung 31: Kapitel 10: Existenz von Gödelsätzen und Präzisierung von Gödels erstem Unvollständigkeitssatz; Anmerkungen zu Hilberts Programm; die Peano-Arithmetik; Formulierung von Gödels zweitem Unvollständigkeitssatz; Hinweise zur Prüfungsvorbereitung. [Flash | QuickTime | Mobile | MP3] (Aufzeichnung vom 13.02.2014)

Termine

	Zeit	Ort	Leitung
Vorlesung	Dienstags 14:15-16:00	Magnus-Hörsaal in der Informatik, Robert-Mayer-Str. 11-15	Prof. Dr. Nicole Schweikardt
Vorlesung	Donnerstags 14:15-16:00	Magnus-Hörsaal in der Informatik, Robert-Mayer-Str. 11-15	Prof. Dr. Nicole Schweikardt
Übung 1	Donnerstags 16:15-18:00	Magnus-Hörsaal in der Informatik, Robert-Mayer-Str. 11-15	Frederik Harwath, Jens Keppeler

Übungsblätter

• Blatt 1 ( ausgeteilt am Do, 17.10.2013 ;  zu bearbeiten bis Do, 24.10.2013 )
• Blatt 2 ( ausgeteilt am Do, 24.10.2013 ;  zu bearbeiten bis Do, 31.10.2013 )
• Blatt 3 ( ausgeteilt am Do, 31.10.2013 ;  zu bearbeiten bis Do, 7.11.2013 )
• Blatt 4 ( ausgeteilt am Do, 7.11.2013 ;  zu bearbeiten bis Do, 14.11.2013 )
• Blatt 5 ( ausgeteilt am Do, 14.11.2013 ;  zu bearbeiten bis Do, 21.11.2013 )
• Blatt 6 ( ausgeteilt am Do, 21.11.2013 ;  zu bearbeiten bis Do, 28.11.2013 )
• Blatt 7 ( ausgeteilt am Do, 28.11.2013 ;  zu bearbeiten bis Do, 12.12.2013 )
• Blatt 8 ( ausgeteilt am Di, 10.12.2013 ;  zu bearbeiten bis Do, 19.12.2013 )
• Blatt 9 ( ausgeteilt am Di, 17.12.2013 ;  zu bearbeiten bis Do, 16.01.2014 )
• Blatt 10 ( ausgeteilt am Do, 16.01.2014 ;  zu bearbeiten bis Do, 23.01.2014 )
• Blatt 11 ( ausgeteilt am Do, 30.01.2014 ;  zu bearbeiten bis Do, 6.02.2014 )
• Blatt 12 ( ausgeteilt am Do, 06.02.2014 ;  zu bearbeiten bis Do, 13.02.2014 )

Prüfungen bzw. Scheine

Vorsicht:

In der Vorlesung und der Übung werden viele wichtige Dinge (insbesondere Beweise, aber auch einiges andere) an der Tafel erklärt. Diese Dinge sind für die Veranstaltung "Logik in der Informatik" wesentlich und daher auch dann prüfungsrelevant, wenn sie nicht in den hier erhältlichen pdf-Dateien enthalten sind.
Zur Vorbereitung auf eine Prüfung (Modulabschlussprüfung) ist es unbedingt notwendig, das gesamte in den Vorlesungs- und Übungsstunden (mit Folien oder an der Tafel) vermittelte Material durchzuarbeiten.

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

Je nach Anzahl der Teilnehmer/innen eine mündliche Prüfung oder eine 180-minütige Klausur.

Im Lauf des Semesters können Bonuspunkte erworben werden, durch deren Einbringen die Note einer bestandenen Modulabschlussprüfung um eine Teilnote verbessert werden kann (also von 4,0 auf 3,7; von 3,7 auf 3,3; von 3,3 auf 3,0; von 3.0 auf 2,7; von 2,7 auf 2,3; von 2,3 auf 2,0; von 2,0 auf 1,7; von 1,7 auf 1,3; von 1,3 auf 1,0).

In der letzten Übungsstunde vor Weihnachten und in der letzten Übungsstunde des Semesters wird je ein 90-minütiger Test geschrieben.
Voraussetzung für den Erwerb von Bonuspunkten, durch deren Einbringen die Note einer bestandenen Modulabschlussprüfung um eine Teilnote verbessert werden kann, sind:

1. Bestehen der beiden des Tests und
2. Erreichen von mindestens 50 Prozent aller Übungspunkte (bitte beachten Sie, dass dies insbes. die regelmäßige und aktive Teilnahme an den Übungsstunden erfordert, siehe unten).

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

In der letzten Übungsstunde vor Weihnachten und in der letzten Übungsstunde des Semesters wird je ein 90-minütiger Test geschrieben.
Voraussetzung für den Scheinerwerb sind:

1. Bestehen der beiden des Tests und
2. Erreichen von mindestens 50 Prozent aller Übungspunkte (bitte beachten Sie, dass dies insbes. die regelmäßige und aktive Teilnahme an den Übungsstunden erfordert, siehe unten).

Verbindliche "Spielregeln" zum Erwerb von Übungspunkten:

Übungsblätter werden donnerstags nach der Vorlesung ausgeteilt. Am Donnerstag der darauf folgenden Woche 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 wie viele Ü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 Situation für den jeweiligen Teilnehmer zum zweiten Mal in diesem Semester auf, so kann er in der Veranstaltung "Logik in der Informatik" im WS 2013/14 keine Übungspunkte erwerben.

Literatur

[S]	N. Schweikardt. Skript zur Vorlesung "Logik in der Informatik", Goethe-Universität Frankfurt am Main, 2011. Link
[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-Logik]	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 Colloqium'81, J.Stearn (editor), pp.105-135. North-Holland Publishing Company, 1982.
[Logicomix]	A. Doxiaidis, C.H. Papadimitriou, A. Papadatos, A. Di Donna. Logicomix: An Epic Search for Truth. Bloomsbury USA, 2009 :  Informationen zu diesem Comic sind hier erhältlich.

Links

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