Details:
Title  Refined program extraction from classical proofs  Author(s)  Ulrich Berger, Wilfried Buchholz, Helmut Schwichtenberg  Type  Article in Journal  Abstract  The paper presents a refined method of extracting reasonable and sometimes unexpected programs from classical proofs of formulas of the form for all x there exists y B. We also generalize previously known results, since B no longer needs to be quantifierfree, but only has to belong to a strictly larger class of socalled "goal formulas". Furthermore we allow unproven lemmas D in the proof of for allxthere existsyB, where D is a socalled "definite" formula.  Keywords  Program extraction; Atranslation; Definite formula  Length  23  ISSN  01680072  Copyright  Copyright © 2002 Elsevier Science B.V. All rights reserved. 
File 
 URL 
http://www.sciencedirect.com/science?_ob=MImg&_imagekey=B6TYB44XVWV727&_cdi=5614&_user=616146&_orig=browse&_coverDate=04%2F15%2F2002&_sk=998859998&view=c&wchp=dGLbVzbzSkWz&md5=80d644c5e4cc6fecc353f9c9cdebc753&ie=/sdarticle.pdf 
Language  English  Journal  Annals of Pure and Applied Logic  Volume  114, Issues 13  Pages  325  Publisher  Elsevier  Year  2002  Month  April  Editor  S.N. Artemov, J.Y. Girard, T. Jech, A. Kechris, U. Kohlenbach, Ph.G. Kolaitis, I. Moerdijk, R.I. Soare, A.J. Wilkie  Edition  0  Translation 
No  Refereed 
Yes 
