050057 VU Theoretische Informatik 2 (2005W)

Die Vorlesung Theoretische Informatik II befasst
sich mit weiterfuehrenden Konzepten der Theoretischen
Informatik, basierend auf der Vorlesung Theoretische
Informatik I. Das Ziel der Vorlesung besteht darin,
die wichtigsten der Informatik zugrundeliegenden
Konzepte kennenzulernen und ihre Relevanz fuer die
Loesung konkreter Fragen im Zusammenhang mit Anwendungen
zu studieren.

Die Vorlesung befasst sich mit vier Themenbereichen:
Berechenbarkeit und Entscheidbarkeit, Komplexitaet,
Praedikatenlogik und Sematik von Programmiersprachen.

Der erste Teil, Berechenbarkeit und Entscheidbarkeit,
weist nach, dass nicht jede beliebige Problemstellung
algorithmisch loesbar ist und geht der Frage nach, wie
algorithmische Berechenbarkeit und Entscheidbarkeit
formal gefasst werden
kann. Hierzu werden mehrere Modelle diskutiert, die
sich alle hinsichtlich ihrer theoretischen Ausdrucksfaehigkeit
als aequivalemt erweisen.

Berechenbarkeit stellt sich nur die Frage nach der
prinzipiellen algorithmischen Loesbarkeit eines Problems
und ignoriert den dafuer noetigen Rechenaufwand.
Komplexitaetstheorie wendet sich genau dieser Frage
zu und studiert die praktische Loesbarkeit bzw.
Unloesbarkeit von Problemen durch Klassifikation des
benoetigten Zeit und/oder Speicheraufwands.

Die Praedikatenlogik, der dritte in der Vorlesung
angesprochene Problemkreis, definiert ein formales System,
mit dessen Hilfe mechanisch gueltige Saetze aus
Axiomen abgeleitet werden koennen. Die Praedikatenlogik
stellt einen Rahmen zur Verfuegung, in dem die
Korrektheit von Programmen verifiziert werden kann.

Der abschliessende Teil der Vorlesung befasst sich mit
formalen Methoden zur Spezifikation der Semantk von
Programmiersprachen und der Verifikation und Validation
von Programmen. Operationelle Semantik, Hoaresche
Semantik, wp-Semantik und denotationelle Semantik werden
in diesem Rahmen vorgestellt.