..
Suche
Hinweise zum Einsatz der Google Suche
Personensuchezur unisono Personensuche
Veranstaltungssuchezur unisono Veranstaltungssuche
Katalog plus
/ fb6 / tcs / teaching /
 

Lehrveranstaltungen der Arbeitsgruppe Mathematische Logik und Theoretische Informatik

Wintersemester 2013/14:

Sommersemester 2013:

  • Lineare Algebra für Informatiker
  • Logik
  • Grundlagen der theoretischen Informatik

Wintersemester 2012/13:

Sommersemester 2012:

Wintersemester 2011/12:

Sommersemester 2011:

Wintersemester 2010/11:

  • Grundlagen der theoretischen Informatik
  • Logik

Regelmässige Vorlesungen

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.