Lehrveranstaltungen der Arbeitsgruppe Mathematische Logik und Theoretische Informatik
Wintersemester 2013/14:
- Diskrete Mathematik für Informatiker
- Seminar für Bachelor Informatik: Modelle der Berechenbarkeit
Sommersemester 2013:
- Lineare Algebra für Informatiker
- Logik
- Grundlagen der theoretischen Informatik
Wintersemester 2012/13:
- Diskrete Mathematik für Informatiker
- Seminar für Bachelor Informatik: Automatentheorie
Sommersemester 2012:
- Lineare Algebra für Informatiker
- Seminar für Bachelor Informatik: Graphentheorie
- Seminar: Konstruktive Analysis
- Logik
- Einführung in das interaktive Beweissystem Coq
Wintersemester 2011/12:
- Diskrete Mathematik für Informatiker
- Grundlagen der theoretischen Informatik
- Ordnungen und Verbände
Sommersemester 2011:
- Berechenbarkeit
- Seminar: Temporale Logik
- Proseminar: Automatentheorie
Wintersemester 2010/11:
- Grundlagen der theoretischen Informatik
- Logik
Regelmässige Vorlesungen
- Grundlagen der theoretischen Informatik
- Berechenbarkeit
- Komplexitätstheorie
- Formale Sprachen
- Theorie der Programmierung I, II, III
- Logik
- Konzepte höherer Programmiersprachen
- Theorie der Scott-Bereiche
Grundlagen der theoretischen Informatik
Das Thema dieser Vorlesung ist eine Einführung in die wichtigsten Gebiete der theoretischen Informatik: Die Theorie der Formalen Sprachen beschäftigt sich mit Methoden zur Überprüfung der syntaktischen Korrektheit von Computerprogrammen, d.h. ob ein Programm nur erlaubte Zeichenfolgen enthält. Die Berechenbarkeitstheorie befasst sich mit der Formalisierung des Algorithmusbegriffs. Ein Algorithmus ist ein Verfahren, das einem Computerprogramm zugrundeliegt.
Berechenbarkeit
Der zentrale Begriff dieser Vorlesung ist der des Algorithmus. Das ist die "Grundidee eines Computerprogramms". Die Frage, ob ein Programm zum geforderten Ergebnis führt, setzt voraus, daß die Korrektheit des zugrundeliegenden Verfahrens nachweisbar ist. Schwieriger zu beantworten ist die Frage, ob ein gegebenes Problem überhaupt lössbar ist. Das erste Ziel der Vorlesung ist es, den Algorithmusbegriff zu formalisieren und eine mathematische Definition für Begriffe wie "algorithmisch lösbar" und "berechenbar" zu finden.
Komplexitätstheorie
In der
Komplexitätstheorie, wird eine Theorie entwickelt, mit der man
Algorithmen entsprechend ihrer Laufzeit oder ihres
Speicherplatzverbrauchs klassifizieren kann.
Inhalt:
- Komplexitätsmaße und -klassen
- polynomiell beschränkte Komplexitätsklassen: die Klassen P, NP und PSPACE; Polynomzeithierarchie und das Problem P=NP?
Formale Sprachen
Die Theorie der formalen Sprachen
entstand Anfang der sechziger Jahre mit der Entwicklung der
ersten Programmiersprachen (z.B. ALGOL60). Jede
Programmiersprache ist durch ihre Syntax (erlaubte
Zeichenfolgen) und Semantik (Bedeutung dieser Zeichenfolgen)
festgelegt und dient dazu, Algorithmen in einer für den Rechner
verständlichen Form zu beschreiben. Die Vorlesung liefert
Methoden zur Behandlung der Probleme, die sich ergeben, wenn
ein Computerprogramm auf seine syntaktische Korrektheit
überprüft werden soll.
Inhalt:
- Chomsky-Hierarchie: reguläre, kontextsensitive, Typ-0-Sprachen, Normalformen, Pumping-Lemmata
- Automaten zur Sprachenerkennnung: endliche Automaten, Kellerautomaten, linear beschränkte Automaten Turingakzeptoren
- Abschluß- und Entscheidbarkeitsfgragen
- unentscheidbare Probleme, Postsches Korrespondenzproblem, Komplexität entscheidbarer Probleme
- Analyseverfahren für kontextfreie Sprachen, LL(k)- und LR(k)-Grammatiken
Theorie der Programmierung I, II, III
Ein wichtiges Problem der
Informatik ist die Überprüfung der semantischen Korrektheit von
Programmiersprachen, d.h. inwieweit ein Programm, das in dieser
Sprache geschrieben ist, "das leistet, was der Programmierer
von ihm verlangt". Die Vorlesung stellt verschiedene formale
Methoden zur Beschreibung der Semantik von Programmiersprachen
vor. Darüberhinaus werden mathematische Kalküle zur
Programmverifikation behandelt.
Inhalt:
- Typsysteme
- Methoden der Semantikbeschreibung
- applikative, imperative und objektorientierte Programmiersprachen
- Beweis von Programmeigenschaften
Diese Vorlesung richtet sich an Studierende der Mathematik und Informatik im Hauptstudium
Logik
Mit Logik und logischem Denken
haben sich über Jahrhunderte Philosophen,
Sprachwissenschaftler, Psychologen und Mathematiker
beschäftigt. Anligen der mathematischen Logik ist einerseits
die Untersuchung der Grundlagen der Mathematik. Zum anderen hat
sie das Ziel, die Sprache der Mathematik und vor allem die
mathematischen Beweise zu formalisieren. Anlaß für das
Interesse der Informatiker an der Logik ist die sogenannte
"Softwarekrise", die durch kritische Fehlalarme in
Verteidigungsprogrammen des US-Militärs ausgelöst wurde.
Daraufhin wurden Kalküle entwickelt, die es dem Programmierer
ermöglichen, Korrektheitsbeweise für umfangreiche
Softwarepakete mit Unterstützung des Rechners auszuführen.
Inhalt:
- Aussagenlogik
- Prädikatenlogik 1. und 2. Stufe
- Herleitungen, natürliches Schließen
- mathematische Theorien
- Resolution, Herbrand-Theorien, Resolutionskalkül
- Logikprogrammierung
- Intuitionistische Logik
Konzepte höherer Programmiersprachen
Die Vorlesung wird auf Englisch gehalten. Sie richtet sich an Studierende der Mathematik und Informatik im Hauptstudium.
Theorie der Scott-Bereiche
Das Ziel dieser Vorlesung ist, eine Einleitung in die Theorie der Scott-Bereiche zu geben, insbesondere eine Übersicht über die Theorie der quantitativen Bereiche. Diese Terminologie umfaßt unlängst entstandene Entwicklungen in der Theorie der Scott-Bereiche mit Anwendungen, die auf Messungen reeller Größen basieren (deswegen die Terminologie "quantitativ" gegenüber dem traditionellen "qualitativen" ordnungstheoretischen Versuch). Insbesonderes beschäftigen wir uns mit neuen Anwendungen in dataflow networks, Logik-Programmierung, Modellen für reellwertige Rechnerarithmetik, Modelle für probabilistische Sprachen und Modelle für Komplexitätsanalyse. Diese Themen sind offensichtlich für Informatik-Studenten interessant. Die theoretischen Grundlagen wurden in der nicht-symmetrischen Topologie entwickelt, wobei verallgemeinde Metriken benutzt werden. Die in der Vorlesung vorgestellte Theorie ist insbesondere für Mathematik-Studenten (auch Lehramt) mit Interesse in Topologie, Verbands- oder Maßtheorie interessant. Die auftretenden Begriffe werden zunächst vertraut erscheinen. Wegen der in Informatikanwendungen charakteristischerweise auftretenden nicht-symmetrischen Topologien müssen aber gegenüber der klassischen Vorgehensweise modifizierte Methoden benutzt werden.