Modulcode:	infBL-01a
Englische Bezeichnung:	Computations and Logic
Modulverantwortliche(r):	Prof. Dr. Thomas Wilke
Turnus:	jedes Jahr im WS (WS22/23 WS23/24 WS24/25)
Präsenzzeiten:	4V 2Ü
ECTS:	8
Workload:	60 Std. Vorlesung, 30 Std. Präsenzübung, 150 Std. Selbststudium
Dauer:	ein Semester
Modulkategorien:	BSc-Inf-A (BSc Inf (21)) BSc-WInf-WP-Inf (BSc WInf (21)) MSc-WInf-WP-Inf (MSc WInf (21))
Lehrsprache:	Deutsch
Voraussetzungen:

Kurzfassung:

Das Modul beantwortet die drei folgenden, grundlegenden Fragen:

• Wie sieht ein einfaches, algorithmisch zugängliches Computermodell aus und wo sind dessen Grenzen?
• 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 sieht ein einfaches, algorithmisch zugängliches Computermodell aus und wo sind dessen Grenzen?

Die Studierenden

• realisieren Funktionen als SSTs, beschreiben formale Sprachen durch DFAs und NFAs
• beschreiben die Semantik von SSTs mathematisch präzise und beweisen die Korrektheit einfacher SSTs
• erklären und wenden grundlegende Konstruktionen und Algorithmen für SSTs an (Produkt, Determinisierung, Minimierung)
• entwickeln eigene einfache Konstruktionen und Algorithmen für SSTs und beweisen deren Korrektheit
• beweisen durch Anwendung eines einfachen Kriteriums, dass Funktionen nicht durch SSTs berechnet werden können

Was können Computer leisten und was nicht und wie verschaffen wir uns Gewissheit darüber?

Die Studierenden

• realisieren Algorithmen als TMs
• beschreiben Berechnungen von TMs mathematisch präzise und beweisen die Korrektheit einfacher TMs
• erklären die Funktionsweise einer universellen TM
• bestimmen in einfachen Fällen, ob ein Problem entscheidbar, aufzählbar oder co-aufzählbar ist
• führen mathematisch präzise Unentscheidbarkeitsbeweise in einfachen Fällen durch

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 sieht ein einfaches, algorithmisch zugängliches Computermodell aus und wo sind dessen Grenzen?

• Funktionen als Abstraktion des Ein-Ausgabe-Verhaltens von Computern
• subsequential transducer (SST) als einfaches Berechnungsmodell
• algorithmische Eigenschaften von SSTs
  
  • Wortproblem, Halteproblem, Leerheitsproblem, Universalitätsproblem entscheidbar
  • unter Komposition und weiteren Operationen abgeschlossen
• deterministischer endlicher Automat (DFA) als Spezialfall (zur Beschreibung des Definitionsbereichs)
• nicht-deterministischer endlicher Automat (NFA) als Spezialfall (zur Beschreibung des Wertebereichs)
• Determinisierung und Minimierung als Beispiele für komplizierte Algorithmen
• Cut-and-Paste-Techniken für endliche Zustandsräume

Was können Computer leisten und was nicht und wie verschaffen wir uns Gewissheit darüber?

• Turingmaschine als idealisiertes Modell eines Computers
• Berechnungen und berechnete Funktion als Semantik
• Church-Turing-These zur Veranschaulichung der Bedeutung des Modells
• Beispiele für komplizierte berechenbare Funktionen und nicht berechenbare Funktionen
• Kodierungen von TM als Möglichkeit, TM als Eingaben zu akzeptieren und zu verarbeiten
• Universelle TM, Analogie zum Interpreter
• Entscheidbarkeit einer Menge als Spezialfall der Berechenbarkeit
• Entscheidbarkeit, Aufzählbarkeit, Co-Aufzählbarkeit und Zusammenhänge
• Halteproblem als fundamentales Beispiel für Unentscheidbarkeit
• Reduktionen als Mittel zum Vergleich
• Weitere Beispiele für die genannten Klassen, mit und ohne Beweise

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. (1992). Theoretische Informatik-kurz gefasst. BI Wissenschaftsverlag.
• Schöning, U. (1987). Logik für Informatiker. Mannheim: BI Wissenschaftsverlag.

Verweise:

Kommentar: