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
