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 条
  • [31] REFINED MODEL FOR THE PASSAGE FROM CLASSICAL TO QUANTUM PHYSICS
    Lupascu, Alexandru
    Halati, Catalin
    UNIVERSITY POLITEHNICA OF BUCHAREST SCIENTIFIC BULLETIN-SERIES A-APPLIED MATHEMATICS AND PHYSICS, 2013, 75 (02): : 187 - 194
  • [32] Existential Inertia and Classical Theistic Proofs
    Oppy, Graham
    RELIGIOUS STUDIES, 2025, 61 (01) : 258 - 262
  • [33] A note on the complexity of classical and intuitionistic proofs
    Baaz, Matthias
    Leitsch, Alexander
    Reis, Giselle
    2015 30TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2015, : 657 - 666
  • [34] Polarized and focalized linear and classical proofs
    Laurent, O
    Quatrini, M
    de Falco, LT
    ANNALS OF PURE AND APPLIED LOGIC, 2005, 134 (2-3) : 217 - 264
  • [35] A Constructive Logic with Classical Proofs and Refutations
    Barenbaum, Pablo
    Freund, Teodoro
    2021 36TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2021,
  • [36] Quantum versus classical proofs and advice
    Aaronson, Scott
    Kuperberg, Greg
    TWENTY-SECOND ANNUAL IEEE CONFERENCE ON COMPUTATIONAL COMPLEXITY, PROCEEDINGS, 2007, : 115 - +
  • [37] Classical Proofs' Essence and Diagrammatic Computation
    Lescanne, Pierre
    Zunic, Dragisa
    NUMERICAL ANALYSIS AND APPLIED MATHEMATICS ICNAAM 2011: INTERNATIONAL CONFERENCE ON NUMERICAL ANALYSIS AND APPLIED MATHEMATICS, VOLS A-C, 2011, 1389
  • [38] THE CLASSICAL MOMENT PROBLEM - HILBERTIAN PROOFS
    LANDAU, HJ
    JOURNAL OF FUNCTIONAL ANALYSIS, 1980, 38 (02) : 255 - 272
  • [39] Classical Proofs for the Quantum Collapsing Property of Classical Hash Functions
    Fehr, Serge
    THEORY OF CRYPTOGRAPHY, TCC 2018, PT II, 2018, 11240 : 315 - 338
  • [40] Classical proofs via basic logic
    Faggian, C
    COMPUTER SCIENCE LOGIC, 1998, 1414 : 203 - 219
12345