Modulcode:	infFLog-01a
Englische Bezeichnung:	Advanced Topics in Logic in Computer Science
Modulverantwortliche(r):	Prof. Dr. Thomas Wilke
Turnus:	unregelmäßig (SS22)
Präsenzzeiten:	2V 2Ü
ECTS:	6
Workload:	30 Std. Vorlesung, 30 Std. Präsenzübung, 120 Std. Selbststudium
Dauer:	ein Semester
Modulkategorien:	MSc-Inf-Theo (MSc Inf (21)) MSc-Inf-WP (MSc Inf (21)) 2F-MEd-Inf-WP (MEd-Hdl Inf (21)) 2F-MA-Inf-WP (2F-MA Inf (21)) TI (MSc Inf (15)) WI (MSc Inf (15))
Lehrsprache:	Deutsch
Voraussetzungen:	infBL-01a infAAK-01a

Kurzfassung:

Das Modul behandelt fortgeschrittene Themen der Logik in der Informatik.

Lernziele:

• Modelltheoretische Konzepte und Sachverhalte erarbeiten und zur Lösung von Vollständigkeitsfragen einsetzen.
• Automatentheoretische Konzepte und Sachverhalte erarbeiten und als Mittel zur Entscheidung logischer Theorien einsetzen.
• Kleine Programme spezifizieren und deren Korrektheit manuell durch den Einsatz von Kalkülen nachweisen.
• Berechnungen kodieren und logisch spezifizieren.
• Verschiedene logische Techniken für die automatische Programmanalyse miteinander kombinieren.

Lehrinhalte:

• Vollständigkeit eines natürlichen Beweissystems [1, 2]
• Entscheidbarkeit der Presburger Arithmetik [3]
• Relative Vollständigkeit des Hoare-Kalküls [4]
• SAT-Solver, SMT-Solver und Programmverifikation [5]

Weitere Voraussetzungen:

Prüfungsleistung:

Portfolio (mit Prüfungsvorleistung Kurzvortrag) bei wenigen Studierenden; schriftliche Abschlussprüfung bei vielen Studierenden.

Lehr- und Lernmethoden:

• Flipped classroom
• Hausaufgaben: Lektüre und Lösen von Übungsaufgaben
• Diskussion von Übungsaufgaben in der Gruppe

Verwendbarkeit:

Nur eins der folgenden Module kann pro Studiengang eingebracht werden: infFLog-01a: Fortgeschrittene Logik in der Informatik, infLICS2-01a: Logic in Computer Science - Advanced oder infAutLog-01a: Automata and Logics.

Literatur:

[1] M. Huth, M. Ryan. 2012. Logic in Computer Science. Cambridge University Press, Cambridge, UK.

[2] H.-D. Ebbinghaus, J. Flum, W. Thomas. 2021. Mathematical Logic, 3rd Ed. Springer, New York.

[3] C. Haase. 2018. A survival guide to Presburger arithmetic, ACM SIGLOG News 5, 3, 67-82.

[4] M. Gordon. 2016. Background reading on Hoare Logic, lecture notes.

[5] L. De Moura, N. Bjørner. 2011. Satisfiability modulo theories: introduction and applications. Communications of the ACM 54, 9, 69-77.

Verweise:

Kommentar:

Alternative Voraussetzungen: Inf-TGI und Inf-LogInf.