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 quantifier-free, but only has to belong to a strictly larger class of so-called "goal formulas". Furthermore we allow unproven lemmas D in the proof of for allxthere existsyB, where D is a so-called "definite" formula.
Keywords	Program extraction; A-translation; Definite formula
Length	23
ISSN	0168-0072
Copyright	Copyright © 2002 Elsevier Science B.V. All rights reserved.
File
URL	http://www.sciencedirect.com/science?_ob=MImg&_imagekey=B6TYB-44XVWV7-2-7&_cdi=5614&_user=616146&_orig=browse&_coverDate=04%2F15%2F2002&_sk=998859998&view=c&wchp=dGLbVzb-zSkWz&md5=80d644c5e4cc6fecc353f9c9cdebc753&ie=/sdarticle.pdf
Language	English
Journal	Annals of Pure and Applied Logic
Volume	114, Issues 1-3
Pages	3-25
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