Extraktion von Programmen aus klassischen Beweisen -Extraction of programs from classical proofs

• Antragsteller: Professor Dr. Helmut Schwichtenberg
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2009 bis 2011
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 108789012

Es ist bekannt, dass sich aus formalen Beweisen Algorithmen zusammen mit einem Beweis ihrer Korrektheit extrahieren lassen. Im allgemeinen ist jedoch bei nicht speziell vorverarbeiteten „nicht-konstruktiven Beweisen die rechnerische Information nur implizit enthalten und es werden spezielle Methoden benötigt, um automatisch einen korrekten Algorithmus zu extrahieren. Zwei solche Methoden sind die „verfeinerte A-Übersetzung , die in der Münchener Logik-Gruppe in den letzten 15 Jahren entwickelt und untersucht wurde, und die „Dialectica Interpretation , die von Gödel vor mehr als 50 Jahren vorgeschlagen wurde. Diese Methoden unterscheiden sich sowohl grundsätzlich als auch durch ihre möglichen Anwendungsbereiche- Ziel des beantragten Projekts ist es, das Verhalten der beiden Methoden zu vergleichen, und zwar unter den folgenden Gesichtspunkten:• Anwendbarkeit,• Effizienz der extrahierten Programme, und• Lesbarkeit der extrahierten Programme.

• DFG-Verfahren: Sachbeihilfen