Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal

Details:

   
TitleRefined program extraction from classical proofs
Author(s) Ulrich Berger, Wilfried Buchholz, Helmut Schwichtenberg
TypeArticle in Journal
AbstractThe 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.
KeywordsProgram extraction; A-translation; Definite formula
Length23
ISSN0168-0072
CopyrightCopyright 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
LanguageEnglish
JournalAnnals of Pure and Applied Logic
Volume114, Issues 1-3
Pages3-25
PublisherElsevier
Year2002
MonthApril
EditorS.N. Artemov, J.-Y. Girard, T. Jech, A. Kechris, U. Kohlenbach, Ph.G. Kolaitis, I. Moerdijk, R.I. Soare, A.J. Wilkie
Edition0
Translation No
Refereed Yes
Webmaster