Refined Program Extraction from Classical Proofs
Ulrich Berger, Wilfried Buchholz and Helmut Schwichtenberg

Abstract
The paper develops a refinement of Gödel's negative- and Friedman's A-translation for classical arithmetic in finite types. The advantages of this refinment are twofold: (1) the negative-translation needs to be applied only partially, (2) the translation applies to an enrichment of arithmetic by free predicate symbols (without decidability assumptions) and axioms of a certain syntactical form (including Horn-formulas). (1) leads to simplified programs, (2) increases the applicability of the system since many notions and facts can be introduced axiomatically which means that proofs need only be partially formalized.

Bib entry


@article{Berger02,
   AUTHOR = {Berger, U. and Buchholz, W. and Schwichtenberg, H.},
   TITLE = {Refined Program Extraction from Classical Proofs},
   JOURNAL = {Annals of Pure and Applied Logic},
   VOLUME = 114,
   PAGES = {3--25},
   year = 2002
} 

Draft copy: [pdf] [ps]