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 条
  • [21] Classical Verification of Quantum Proofs
    Ji, Zhengfeng
    THEORY OF COMPUTING, 2019, 15
  • [22] Classical Proofs of Quantum Knowledge
    Vidick, Thomas
    Zhang, Tina
    ADVANCES IN CRYPTOLOGY - EUROCRYPT 2021, PT II, 2021, 12697 : 630 - 660
  • [23] Short proofs of classical theorems
    Bondy, JA
    JOURNAL OF GRAPH THEORY, 2003, 44 (03) : 159 - 165
  • [24] Probabilistic Proofs of Classical Theorems
    Burdzy, Krzysztof
    BROWNIAN MOTION AND ITS APPLICATIONS TO MATHEMATICAL ANALYSIS: ECOLE D'ETE DE PROBABILITES DE SAINT-FLOUR XLIII - 2013, 2014, 2106 : 11 - 19
  • [25] Classical Proofs as Parallel Programs
    Aschieri, Federico
    Ciabattoni, Agata
    Genco, Francesco A.
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (277): : 43 - 57
  • [26] Polarization of classical proofs and reversion
    Quatrini, M
    DeFalco, LT
    COMPTES RENDUS DE L ACADEMIE DES SCIENCES SERIE I-MATHEMATIQUE, 1996, 323 (02): : 113 - 116
  • [27] Light functional interpretation - An optimization of Godel's technique towards the extraction of (more) efficient programs from (classical) proofs
    Hernest, MD
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2005, 3634 : 477 - 492
  • [28] Classical Verification of Quantum Proofs
    Ji, Zhengfeng
    STOC'16: PROCEEDINGS OF THE 48TH ANNUAL ACM SIGACT SYMPOSIUM ON THEORY OF COMPUTING, 2016, : 885 - 898
  • [29] Efficient Extraction of Skolem Functions from QRAT Proofs
    Heule, Marijn J. H.
    Seidl, Martina
    Biere, Armin
    2014 FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD), 2014, : 107 - 114
  • [30] Extraction of proofs from the clausal normal form transformation
    de Nivelle, H
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2002, 2471 : 584 - 598
12345