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?
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
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
Klausur, als Vorleistungen müssen Hausaufgaben (Übungsaufgaben) erfolgreich bearbeitet werden.
Vorlesung, Arbeits- und Fragestunden, Selbststudium.
-
Schöning, U. (1992). Theoretische Informatik-kurz gefasst. BI Wissenschaftsverlag.
-
Schöning, U. (1987). Logik für Informatiker. Mannheim: BI Wissenschaftsverlag.