Materielle Interpretation

Mathematische Beweise erklären, warum bestimmte Aussagen wahr sind und andere nicht. Oft bleiben diese Beweise jedoch sehr theoretisch. Das Projekt Materielle Interpretation will aus diesen theoretischen Beweisen praktische Werkzeuge zur Lösung konkreter Probleme gewinnen. Das Hauptziel besteht darin, Algorithmen aus mathematischen Beweisen zu extrahieren. Wenn zum Beispiel ein Beweis für eine Aussage der Form Für jedes x gibt es ein y mit der Eigenschaft P. gegeben ist, dann wollen wir nicht nur eine abstrakte Existenzaussage erhalten, sondern tatsächlich eine Funktion f, die für jedes x ein konkretes y = f(x) mit der Eigenschaft P konstruiert. Auf diese Weise werden abstrakte mathematische Beweise mit Leben gefüllt und erhalten praktische Anwendungen. Hierfür bedienen wir uns der sogenannten Beweisassistenten. Dabei handelt es sich um Programme, mit deren Hilfe man formale Beweise am Computer führen, speichern und mit ihnen weiterarbeiten kann. Insbesondere kann man Beweisinterpretationen auf die formalen Beweise anwenden. Beweisinterpretationen sind Algorithmen, die man auf Beweise anwendet, um entweder Funktionen wie zum Beispiel die oben beschriebene Funktion f zu gewinnen oder um andere Beweise beispielsweise für allgemeinere oder konstruktivere Aussagen zu erhalten. Ein großer Teil des Projektes wird es sein, eine eigenständige Beweisinterpretation zu entwerfen: Die materielle Interpretation soll möglichst nahe am ursprünglichen Beweis bleiben, aber dennoch mehr konstruktiven Gehalt liefern. Zum Beispiel soll ein Beweis für eine Aussage A impliziert B nach Möglichkeit in eine Aussage der Form nicht A oder B umgewandelt werden. Letztere Aussage ist konstruktiv stärker, da in jedem Fall entschieden werden muss, ob nicht A oder B gilt. Ziel ist es, die materielle Interpretation für eine möglichst große Klasse von Aussagen bzw. Beweisen zugänglich zu machen. Diese Klasse wird Beweise enthalten, deren materielle Interpretation offene Probleme löst, wie z.B. eine neue konstruktive Variante von Hilberts 17. Problem. Um die Ziele des Projekts zu erreichen, werden wir insbesondere die Spezialisierungen und Vorteile verschiedener Beweisassistenten nutzen. Dazu werden wir die Vor- und Nachteile der Beweisassistenten gegenüberstellen und den jeweils nützlichsten Beweisassistenten verwenden. Darüber hinaus wird eine entsprechende Übersicht dazu beitragen, die einzelnen Beweisassistenten zu erweitern und ihre Zusammenarbeit untereinander zu verbessern.