Mathematik

Mit der Beweistheorie aus der Logik in der Mathematik das Unendliche darstellen

Uschi Sorz | aus HEUREKA 2/13 vom 29.05.2013

Der Brückenschlag zwischen Mathematik und Informatik lag bei Stefan Hetzl nahe. "Schon als Kind hat mich die virtuelle Welt der Computer fasziniert", erzählt der 31-Jährige, der zunächst an der Wiener TU Informatik studiert hat.

Weil er dabei aber bald feststellte, dass ihn die Theorie am meisten anzog, hängte er noch ein Mathematikstudium in Wien und Paris an. Sein heutiges Spezialgebiet ist die Logik. "Viel theoretischer geht's wohl nicht", lächelt er. "Sie ist ja sozusagen die Lehre vom Denken selbst. Man sollte allerdings nicht vergessen, dass die meisten Anwendungen auf Grundlagenerkenntnissen basieren. Es gibt nichts Praktischeres als eine gute Theorie." Denn eine solche sagt uns etwas Fundamentales über die Wirklichkeit.

Seit April baut er an der TU Wien mit einer Förderung von 1,5 Mio. Euro eine Forschungsgruppe auf. Er ist einer der beiden Preisträger des "Vienna Research Groups for Young Investigators Call" des WWTF-Schwerpunkts "Mathematik und... ". Hetzls Projekt zielt auf ein besseres Verständnis induktiver Beweise ab und könnte dadurch in der Softwareverifikation Anwendung finden. "Wenn man etwas über ein Computerprogramm aussagen will, muss man in irgendeiner Weise induktive Beweise verwenden", erklärt er. Mittels der Theorie formaler Sprachen wie Computer- oder Programmiersprachen wird seine Gruppe induktive Beweise analysieren und dazu auch die Verbindung zwischen der Beweistheorie und der Theorie formaler Sprachen weiter ausbauen.

Bei Computertests kann man in der Realität nur endlich viele Eingaben tätigen, während die Möglichkeiten unendlich sind. "Induktive Beweise erlauben es aber, mit endlichen Ausdrücken etwas über unendliche Objekte auszusagen", sagt Hetzl.

Weitere Artikel lesen


Anzeige

Anzeige