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
 

Project Description

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