Die Feinstruktur von formalen Beweissystemen und ihre computationalen Interpretationen

Das Projekt Die Feinstruktur von formalen Beweissystemen und ihre computationalen Interpretationen (FISP) stellt eine Fortsetzung des STRUKTURELL Projektes (2011-2014) dar, dessen Gesamtziel die Anwendung von Methoden der mathematischen Logik in der Informatik war. FISP wird sich auf die Weiterentwicklung der Forschungsziele konzentrieren, die im STRUKTURELL Projekt besonders erfolgreich waren. Das Hauptaugenmerk liegt deshalb auf dem Studium formaler Beweise und der Extraktion des algorithmischen Gehalts aus Beweisen, unter letzterem versteht man, dass die implizite Konstruktionen, die in einem mathematischen Argument verwendet werden, explizt angegeben werden können, gegebenenfalls gelingt dies sogar automatisch. Zum Beispiel kann man aus dem Beweis der Wohldefiniertheit einer Spezifikation einen Algorithmus, der diese Spezifikation erfüllt, extrahieren. Das Projekt ist eine Zusammenarbeit von vier Partnerinstitutionen, zwei österreichischen und zwei französischen, deren Arbeiten auf dem Gebiet der strukturellen Beweistheorie international annerkannt sind, die jedoch aus verschiedenen Traditionen kommen. Einerseits vertreten die Projektpartner die mathematische Tradition, andererseits Traditionen der Informatik. Eine Gemeinsamkeit dieser Traditionen ist die überragende Rolle, die elementare Beweise und Beweistransformationen spielen. Das FISP Projekt ist Teil des langfristigen und ambitioniertes Projektes, die mächtigen und vielversprechenden Methoden der mathematischen Logik auf Probleme der Informatik anzuwenden, auf welche sie bis dato nicht angewandt wurden, etwa der algorithmische Gehalt von Beweisen, die Extraktion von Programmen aus Beweisen und die logische Kontrolle von verfeinerten algorithmischen Operationen. Derzeit werden etwa Arbeiten zum algorithmischen Gehalt von Beweisen mehrheitlich mittels der von Gentzen in den 1930er Jahren entwickelten Methoden durchgeführt. Allerdings stößt dieser Ansatz an seine Grenzen, wenn es darum geht die algorithmische Bedeutung der klassischen Logik darzulegen oder nebenläufige bzw. verteilte Verarbeitung zu studieren. Das Ziel des Projektes ist es, aufbauend auf der komplementären Kompetenz der Partner, diese Grenzen zu überwinden indem neueste Forschungserkenntnisse auf die Fragestellungen im Projekt adaptiert werden. Das STRUKTURELL Projekt hat den Nachweis erbracht, dass die gewählte Methodologie und die ausgesuchen Forschungsziele sinnvoll sind. Die gemeinsame Expertise führte zu bemerksenswerten Ergebnissen in drei thematischen Bereichen des FISP Projektes, sodass neue Forschungsbereiche von allgemeinem Interesse eröffnet werden konnten. Diese Resultate zeigen das Potential und die Relevanz der gewählten Methoden. Das FISP Projekt führt die theoretische Entwicklung dieser Techniken fort und wird neue Anwendungen im Rahmen der logischen Modellierung von Berechnungen liefern. Primärziele sind die logische Modellierung von abstrakten Maschinen, sowie nebenläufige und verteilte Berechnungen.

Die Feinstruktur formaler Beweissysteme und ihre computationale Interpretation (FISP). Das Ziel des FISP Projektes kann wie folgt zusammengefasst werden. FISP untersucht die Feinstruktur formaler Beweissysteme auf drei verschränkten Ebenen: *) auf der Ebene von Beweisformalismen, die Berechnungen zugrundeliegen; *) auf der Ebene der logischen Kontrolle; *) auf der Ebene neuer logischer Modelle der Berechenbarkeit. Das FISP Projekt ist Teil eines langfrstigen, ambitionierten Projektes, dessen Ziel es ist die mächtigen und vielversprechenden Werkzeuge der strukturellen Beweistheorie auf zentrale Probleme in der Informatik in neuartiger Weise anzuwenden. Im Besonderen zielt unser Interesse auf das Verständnis des computationalen Gehalts von Beweisen, der Extraktion von Programmen und der logischen Kontrolle verfeinerter computationaler Operatrionen ab. Immer noch bezieht sich die Forschung auf dem Gebiet der computatonalen Interpretation von logischen Systeme auf die herausragenden Arbeiten von Gentzen, der in den 1930ern den Sequentialkalkül und das natürliche Schließen, sowie die Schnittelimination eingeführt hatte. Aber dieser Ansatz zeigt seine Grenzen, wenn es um die computationale Interpretation klasischer Logik geht oder die Modellierung von Parallelverarbeitung. Das Ziel dieses Projektes ist es, basierende auf die komplementäre Stärke des Consortiums, diese Beschränkungen zu überwinden. Zum Beispiel bietet die tiefe Inferenz neue Eigenschaften, wie volle Symmetrie und Atomizität, die bisher nicht verfügbar waren und eröffnet somit neue Möglichkeiten auf der Ebene der Berechenbarkeit, etwa in Bezug auf Parallelverarbeitung von verteiltes Rechnen. Hauptresultate. Genau wie das vorangegangene STRUCTURAL Projekt, hat das gerade beendete FISP Projekt demonstriert, dass die verwandte Methodologie und die gewählten Forschungsschwerpunkte passgenau sind. Die gemeinsame Expertise des Forschungsteams hat zu herausragenden Forschungserfolgen auf den Gebieten des FISP Projekts geführt und neue Forschungsfelder von großem Interesse eröffnet. Zum Bespiel wurden neue Formen von Millers Expansionsbäumen mit Schnitten entwickelt, nicht-elementary Beschleunigungen von Beweisen mit der Hilfe von (lokal) inkorrekten Inferenzeregeln erzielt und Studien zu unteren und oberen Schranken der Länge von Herbranddisjunktionen, basierend auf der Formalisierung von Beweisen in Hilberts Epsilonkalkül, finalisert. Faktische Informationen. Das FISP Projekt war ein internationales Projekt der Grundlagenforschung, koordiniert durch Michel Parigot (Universität Paris-Diderot). Es bringt Teams der (i) Universität Innsbruck, (ii) der Technischen Universität Wien, (iii) INRIA Saclay und (iv) der Universität Paris-Diderot zusammen. Die österreichische Seite wurde von Georg Moser (Universität Innsbruck) koordiniert. Das Projekt startete am 1. Jänner 2016 und dauerte 42 Monate. Es profitierte von einer FWF Förderung von EUR 310.842,-.