Es ist bekannt, daß sich Programme aus formalen Beweisen extrahieren lassen. Die theoretischen Grundlagen hierzu sollen unter folgenden Aspekten untersucht werden. 1. Effizienz der extrahierten Programme; 2. Programmextraktion aus klassischen Beweisen, mit besonderer Berücksichtigung der rolle von Fixpunkt- und Kontrolloperatoren, und 3. Einbeziehung der Beweistheorie undendlicher Herleitungen Parallel dazu soll die prototypische Implementierung MINLOG weiterentwickelt und damit Fallstudien durchgeführt werden.
DFG Programme
Research Grants
