Zum Hauptinhalt springen

Theoretische Informatik

Die Informatik ist eine theoretische Wissenschaft. Sie

„befaßt sich mit vom Menschen geschaffenen Objekten. Wir müssen zuerst erdenken oder erbauen, was wir dann untersuchen wollen. Wir müssen die intellektuellen Werkzeuge entwickeln, mit denen wir nicht nur das Existierende erforschen, sondern auch das Mögliche studieren können“ (Juris Hartmanis)

Aber was können wir konstruieren? Verhält sich das, was wir konstruiert haben, auch so, wie wir es erwarten? Computer verändern unser Leben. Bereichern sie es auch? Wissen wir, was die vom Menschen geschaffenen Artefakte tun, was sie vermögen und wo ihre Grenzen sind?

Diese Fragen berühren die Grundlagen der Wissenschaft Informatik. Ihre Beantwortung ist schwierig und fordert den Einsatz ausgefeilter Hilfsmittel aus der Mathematik. Häufig sind die Problemstellungen mit den vorhandenen Hilfsmitteln nicht zu bewältigen und neue mathematische Werkzeuge müssen entwickelt und für die Behandlung der Probleme der Informatik angepaßt werden.

Am Lehrgebiet Theoretische Informatik werden aus diesem breiten Spektrum von Problemen vorrangig zwei Problemkreise bearbeitet:

Formale Methoden in der Programmierung

In diesem Problemkreis geht es um den Entwurf systematischer Methoden zur Synthese, Verifikation und Optimierung von Algorithmen und Softwaresystemen. Ein besonderer Schwerpunkt liegt auf Methoden, die sich in logischen Kalkülen beschreiben und somit mit Hilfe von interaktiven und automatischen Beweisverfahren implementieren lassen, und auf der Anwendung derartiger Methoden in der Entwicklung zuverlässiger und effizienter Software.

Automatisierung von Beweisverfahren

Beweiskalküle für ausdruckstarke Logiken sind prinzipiell in der Lage, jedes Beweisproblem zu formalisieren und zu präzisieren. Ein praktisches Problem in der logischen Beweisführung ist jedoch die Größe der resultierenden Beweise. Während interaktive Beweissysteme ein sehr gutes Hilfsmittel für die fehlerfreie Konstruktion formaler Beweise sind, macht der Aufwand, derartige Beweise zu finden, eine interaktive Beweiskonstruktion für komplexe Beweisziele unpraktikabel. Vollautomatische Beweisprozeduren dagegen gibt es zur Zeit nur für relativ ausdrucksschwache Logiken. Ziel unserer Arbeit ist daher die Entwicklung automatischer Beweisverfahren für ausdrucksstärkere Logiken, die sich zur Steuerung der Beweiskonstruktion in interaktiven Beweissystemen eignen.