Refined program extraction from classical proofs

被引：34
|
作者：
Berger, U
Buchholz, W
Schwichtenberg, H
机构：
[1] Univ Munich, Inst Math, D-80333 Munich, Germany
[2] Univ Coll Swansea, Dept Comp Sci, Swansea SA2 8PP, W Glam, Wales
来源：
ANNALS OF PURE AND APPLIED LOGIC | 2002年 / 114卷 / 1-3期
关键词：
program extraction; A-translation; definite formula;
D O I：
10.1016/S0168-0072(01)00073-2
中图分类号：
O29 [应用数学];
学科分类号：
070104 ;
摘要：
The paper presents a refined method of extracting reasonable and sometimes unexpected programs from classical proofs of formulas of the form For AllxThere ExistsyB. 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. (C) 2002 Elsevier Science B.V, All rights reserved.
引用
收藏
页码：3 / 25
页数：23
相关论文
共 50 条
12345