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

• Applicant: Professor Dr. Helmut Schwichtenberg
• Subject Area: Theoretical Computer Science
• Term: from 2009 to 2011
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 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 Programme: Research Grants