STRUKTURELL

Dieses Projekt ist eine Zusammenarbeit von vier Partnerinstitutionen, zwei französischen und zwei österreichischen, deren Arbeiten auf dem Gebiet der strukturellen Beweistheorie international annerkannt sind, die jedoch aus verschiedenen Traditionen kommen. Eines der Ziele dieses Projektes ist es eine Brücke zu schlagen zwischen diesen Traditionen, um neue Werkzeuge und Techniken für die strukturelle Beweistheorie zu entwickeln. Diese haben ein großes Potential für Anwendungen im Bereich der Informatik, im Besonderen in den Bereichen Berechenbarkeit, Extraktion von Programmen und Beweiskomplexität. Auf der einen Seite vertreten die Projektpartner eine Tradition, die aus der Mathematik kommt und sich hauptsächlich mit dem Studium der erststufigen Logik beschäftigt. Diese Richtung studiert etwa Herbrands Theorem, Hilberts Epsilon Kalkül, oder Gödels Dialectica Interpretation. Auf der anderen Seite repräsentieren die Projektpartner eine Tradition, die sich in der Informatik entwickelt hat. Diese ist mehrheitlich mit propositionalen Systemen beschäftigt und studiert etwa den Curry-Howard Isomorphismus, algebraische Semantik, lineare Logik, Beweisnetze oder tiefe Inferenz. Eine Gemeinsamkeit dieser Traditionen ist die überragende Rolle, die analytische Beweise und Schnitt-Elimination spielen. Wir werden das Zusammenspiel dieser Traditionen studieren, im Besonderen werden wir die Bereiche der tiefen Inferenz, Curry-Howard Isomorphismus, Termersetzung und Hilberts Epsilonkalkül untersuchen. Als Nebenprodukt wird dieses Projekt einen fruchtbaren Austausch zwischen diesen beiden, auf gemeinsamen Grund stehenden, Forschungsgemeinden erzielen. Wir werden etwa den Zusammenhang von Herbrand Expansionen und der computatonalen Interpretation von Beweisen studieren, sowie die Bedeutung des Epsilonkalküls in der Beweiskomplexität. Neben den bekannten, aber noch immer nicht völlig ausgeschöpften Werkzeugen der Beweistheorie, wie dem Epsilonkalkül oder der Dialectica Interpretation wird das Hauptarbeitszeug unserer Untersuchungen tiefe Inferenz sein. Tiefe Inferenz ermöglicht die Anwendung von Inferenzregeln tief in einer Formel, innerhalb eines beliebigen Kontexts. Diese nderung in der Anwendbarkeit von Inferenzregeln hat drastische Effekte auf die meisten grundlegenden beweistheoretischen Eigenschaften von Systemen, wie etwa Schnittelimination. Folglich waren viele der früheren Resultate in diesem Gebiet darauf bezogen bekannte, fundamentale Resultate erneut zu beweisen. Nun ist tiefe Inferenz allerdings ein ausreichend entwickeltes Gebiet, sodass an Anwendungen gedacht werden kann. Tiefe Inferenz erzielt neue Eigenschaften, die in Standardkalkülen nicht möglich wären, nämlich volle Symmetrie und Atomizität. Dies erweitert den Gestaltungsraum auf der computationalen Ebene, welche wir in diesem Projekt ebenfalls untersuchen werden. Darüberhinaus wollen wir den genauen Zusammenhang zwischen tiefer Inferenz und Termersetzung studieren und hoffen auch eine generelle Theorie analytischer Kalküle in tiefer Inferenz entwickeln zu können.

Strukturelle und computationale Beweistheorie Das Ziel des STRUKTURELL Projekt lässt sich wie folgt zusammenfassen:Strukturelle und computationale Beweistheorie untersucht die Feinstruktur formaler Beweise in einem algorithmischen Sinne.Das STRUKTURELL Projekt beschäftigte sich mit der Erfassung des algorithmischen Gehalts von Beweisen, der Programmextraktion aus Beweisen und der Verbesserung von Programmierparadigmen durch die Verfeinerung der logischen Kontrolle über Berechnungsoperatoren. Es wurde durch ein Konsortium von vier Partnern, zwei österreichischen und zwei französischen, durchgeführt, die alle international auf dem Gebiet der strukturellen Beweistheorie ausgewiesen sind, aber aus unterschiedlichen Traditionen stammen. Die Hauptidee des Projektes ist die Anwendung von mächtigen und vielversprechenden Werkzeugen der strukturellen Beweistheorie - im Besonderen tiefe Inferenz, Herbranddisjunktionen und Hilberts ?-Kalkül- auf informatische Probleme, im Besonderen aus dem Bereich der Programmiersprachen, für welche sie noch nicht verwandt wurden. Die Methode kann auf zwei Arten beschrieben werden, welche die beiden Seiten der Korrespondenz zwischen Beweisen und Programmen, genannt Curry-Howard Korrespondenz, darstellt. Wenn man die Blickrichtung der Informatik benutzt, dann geht es darum mit Hilfe von logischen Systemen algorithmische Operationen zu typisieren. Benutzt man aber die Blickrichtung der Logik, dann geht es darum neue computationale Interpretationen von Beweissystemen zu erlangen, die entweder bekannten oder völlig neuen Berechnungsmodellen entsprechen. Der gemeinsame Idee ist es, die Beschränkungen traditioneller logische Systeme, etwa im Bereich der Analyse von Programmiersprachen, durch die Einführung von Symmetrieeigenschaften und Atomizität sowie der Reduktion von Quantoren auf Terme, zu überwinden.Hauptresultate Die gemeinsame Expertise der Forschungsteams hat zu bemerkenswerten Fortschritten in 3 Hauptthemen des Projekts geführt. Dadurch wurden neue Forschungsfelder von großem Interesse geschaffen. Etwa wurde gezeigt dass algorithmische Interpretationen der tiefen Inferenz eine adequate Typisierung des ?-Kalküls mit explizitem Sharing sowie von Interaktionsnetzen erlaubt. Es wurde überraschenderweise gezeigt, dass der Nichtdeterminismus der algorithmischen Interpretation klassischer Logik durch Herbrandformeln kontrolliert werden kann. Schließlich wurde eine neue Charakterisierung der endlichweiten Gödellogiken mit Hilfe von Hilberts ?-Kalkül erreicht. Fakten Das STRUKTURELL Projekt war ein internationales Projekt der Grundlagenforschung, welches von Michel Parigot (Labor PPS, Universität Paris-Diderot) koordiniert wurde. Es brachte Forschungsgruppen der Universität Innsbruck, der TU Wien, von INRIA Saclay, sowie der Universität Paris-Diderot zusammen. Die österreichische Projektseite wurde von Georg Moser (Universität Innsbruck) koordiniert. Das Projekt begann am 1. Februar 2011 und dauerte 38 Monate; es profitierte von einer FWF Förderung in der Höhe von 314.000,-.