Modulcode:	infBL_L-01a
Englische Bezeichnung:	Computations and Logic - Logic Part
Modulverantwortliche(r):	Prof. Dr. Thomas Wilke
Turnus:	jedes Jahr im WS (WS23/24)
Präsenzzeiten:	2V 1Ü
ECTS:	4
Workload:	30 Std. Vorlesung, 15 Std. Präsenzübung, 75 Std. Selbststudium
Dauer:	ein Semester
Modulkategorien:	BSc-Inf-A (BSc Inf (21))
Lehrsprache:	Deutsch
Voraussetzungen:

Kurzfassung:

Das Modul beantwortet die drei folgenden, grundlegenden Fragen:

• Was können Computer leisten und was nicht und wie verschaffen wir uns Gewissheit darüber?
• Wie lassen sich Sachverhalte deklarativ beschreiben und deduktiv analysieren? Innerhalb welcher Grenzen kann das erfolgen?

Lernziele:

Abkürzungen

• SST = subsequential transducer
• DFA = deterministic finite-state automaton
• NFA = non-deterministic finite-state automaton
• TM = Turing machine
• FOL = first-order logic

Die Lernziele gliedern sich in die folgenden grundlegenden Fragen der theoretischen Informatik:

Wie lassen sich Sachverhalte deklarativ beschreiben und deduktiv analysieren? Innerhalb welcher Grenzen kann das erfolgen?

Die Studierenden

• konstruieren einfache FO-Strukturen
• definieren die Syntax und Semantik der FOL
• überprüfen grundlegende Eigenschaften von FOL-Formeln unter Rückgriff auf die Semantik (Gültigkeit, Erfüllbarkeit, Äquivalenz, Folgerung)
• entwickeln einfache Axiomensysteme und erläutern wichtige Axiomensysteme
• definieren Relationen in Strukturen durch FOL-Formeln
• wenden logische Gesetze an und erstellen Formeln in Normalformen
• beweisen den Zusammenhang zwischen Erfüllbarkeit und Folgerung
• modellieren einzelne komplexe Sachverhalte und beweisen die Unentscheidbarkeit von Erfüllbarkeit und Folgerung
• erklären die Resolutionsregel, beweisen deren Korrektheit und entwickeln Resolutionsbeweise
• erklären, dass Erfüllbarkeit und Folgerung co-aufzählbar bzw. aufzählbar sind

Lehrinhalte:

Wie lassen sich Sachverhalte deklarativ beschreiben und deduktiv analysieren? Innerhalb welcher Grenzen kann das erfolgen?

• Formeln als Mittel zur Beschreibung von Sachverhalten
• Prädikatenlogik als Sprache, die sich an die Logik in der natürliche Sprache anlehnt
• Strukturen, Syntax, Semantik (Modellbeziehung)
• Axiomensysteme (Theorien)
• Abfragen, um deklarativ Eigenschaften zu beschreiben
• Äquivalenz, Gesetze, Normalformen, Substitution
• Folgerungsbeziehung als logischer Schluss
• Erfüllbarkeit und Zusammenhang zur Folgerung
• Modellierung komplexerer Sachverhalte und Unentscheidbarkeit der Erfüllbarkeit
• Resolution als vollständiges Kalkül
• Ausblick: SMT-Solver

Weitere Voraussetzungen:

Prüfungsleistung:

Klausur, als Vorleistungen müssen Hausaufgaben (Übungsaufgaben) erfolgreich bearbeitet werden.

Lehr- und Lernmethoden:

Vorlesung, Arbeits- und Fragestunden, Selbststudium.

Verwendbarkeit:

Literatur:

• Schöning, U. (1987). Logik für Informatiker. Mannheim: BI Wissenschaftsverlag.

Verweise:

Kommentar:

Dieses Modul wird ist kein offizieller Bestandteil eine Prüfungsordnung. Es ist insbesondere für die Umsetzung von Übergangsregelungen zur FPO 2021, bzw. dem ab dem Sommersemester 2023 gelesenen Modul infBL-01a: Berechungen und Logik.

Außerdem wird das Modul im Rahmen der Anmeldung zur Teilnahme am Modul infBL-01a: Berechungen und Logik verwendet.