Logik in der Informatik (212013-SS 2024)

Logische Methoden spielen in vielen modernen Anwendungen der Informatik eine wichtige Rolle. Aus Datenbanken werden relevante Informationen  mit Hilfe auf Logik basierender Anfragesprachen extrahiert; die formale Verifikation von Software und Hardware basiert auf logischen Spezifikationssprachen und Algorithmen für diese; und Methoden für das automatisierte Schlussfolgern in der künstlichen Intelligenz haben ihre Grundlage in der formalen Logik.

In dieser Veranstaltung werden die formalen Grundlagen von modernen Logiken behandelt, mit einem Fokus auf ihrer Anwendung in der Informatik. Neben der klassischen Aussagenlogik und Prädikatenlogik betrachten wir auch Modallogik.  Für jede dieser Logiken formalisieren wir Syntax und Semantik, lernen wie sich informatische Szenarien in ihnen modellieren lassen, und betrachten Algorithmen und Kalküle für Unerfüllbarkeit und Folgerungsbeziehung.

Einstiegsliteratur für diese Veranstaltung sind die Bücher:

• M. Kreuzer and S. Kühling. Logik für Informatiker. Pearson, 2006
• Uwe Schöning. Logik für Informatiker. Spektrum Akademischer Verlag, 2000

Lernziele  
Die Studierenden lernen, wie sich Problemstellungen durch geeignete logische Systeme modellieren lassen. Sie sollen Syntax und Semantik verschiedener logischer Systeme beherrschen und nutzen können. Sie sollen einige klassische logische Kalküle und Algorithmen kennen sowie diese durchführen können. Sie sollen weiterhin ein grundlegendes Verständnis für die Logik-Programmierung entwickeln und insbesondere  einfache Sachverhalte durch Prolog-Programme auszudrücken können.