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 条

[11] PROOFS AND PROGRAMS - A NAIVE APPROACH TO PROGRAM EXTRACTION
NAKAHARA, H
PUBLICATIONS OF THE RESEARCH INSTITUTE FOR MATHEMATICAL SCIENCES, 1989, 25 (03) : 415 - 489
[12] Light Dialectica Program Extraction from a Classical Fibonacci Proof
Hernest, Mircea-Dan
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 171 (03) : 43 - 53
[13] Classical program extraction in the calculus of constructions
Miquel, Alexandre
Computer Science Logic, Proceedings, 2007, 4646 : 313 - 327
[14] AN INTERPRETATION OF CLASSICAL PROOFS
HELMAN, G
JOURNAL OF PHILOSOPHICAL LOGIC, 1983, 12 (01) : 39 - 71
[15] Getting results from programs extracted from classical proofs
Raffalli, C
THEORETICAL COMPUTER SCIENCE, 2004, 323 (1-3) : 49 - 70
[16] Proofs of God: Classical Arguments from Tertullian to Barth
Siniscalchi, Glenn B.
REVIEW OF METAPHYSICS, 2019, 72 (03): : 606 - 607
[17] Proofs of God: Classical Arguments from Tertullian to Barth
Schenkewitz, Kyle A.
NEWMAN STUDIES JOURNAL, 2018, 15 (02) : 79 - 80
[18] Programs from proofs using classical dependent choice
Seisenberger, Monika
ANNALS OF PURE AND APPLIED LOGIC, 2008, 153 (1-3) : 97 - 110
[19] A Symmetric Lambda Calculus for Classical Program Extraction
Dipartimento di Informatica, Università di Torino, Corso Svizzera, 185, 10149 Torino, Italy
Inf Comput, 2 (103-117):
[20] A symmetric lambda calculus for classical program extraction
Barbanera, F
Berardi, S
INFORMATION AND COMPUTATION, 1996, 125 (02) : 103 - 117

← 1 2 3 4 5 →