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 条
  • [41] CONSISTENCY PROOFS OF SUBSYSTEMS OF CLASSICAL ANALYSIS
    TAKEUTI, G
    ANNALS OF MATHEMATICS, 1967, 86 (02) : 299 - &
  • [42] Naming proofs in classical propositional logic
    Lamarche, F
    Strassburger, L
    TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS, 2005, 3461 : 246 - 261
  • [43] The duality of classical and constructive notions and proofs
    Negri, Sara
    von Plato, Jan
    FROM SETS AND TYPES TO TOPOLOGY AND ANALYSIS: TOWARDS PRACTICABLE FOUNDATIONS FOR CONSTRUCTIVE MATHEMATICS, 2005, 48 : 149 - 161
  • [44] Extraction of Defeasible Proofs as Explanations
    Pasetto, Luca
    Cristani, Matteo
    Governatori, Guido
    Olivieri, Francesco
    Zorzi, Edoardo
    CEUR Workshop Proceedings, 2023, 3546
  • [45] Convincing Proofs for Program Certification
    Garnacho, Manuel
    perin, Michael
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 238 (04) : 41 - 56
  • [46] CLASSICAL PROOFS AS PROGRAMS - HOW, WHAT AND WHY
    MURTHY, CR
    LECTURE NOTES IN COMPUTER SCIENCE, 1992, 613 : 71 - 88
  • [47] Classical proofs, typed processes, and intersection types
    Ghilezan, S
    Lescanne, P
    TYPES FOR PROOFS AND PROGRAMS, 2004, 3085 : 226 - 241
  • [48] Proofs and Countermodels in Non-Classical Logics
    Negri, Sara
    LOGICA UNIVERSALIS, 2014, 8 (01) : 25 - 60
  • [49] Normal Natural Deduction Proofs (in classical logic)
    Wilfried Sieg
    John Byrnes
    Studia Logica, 1998, 60 (1) : 67 - 106
  • [50] Abstract interpretation of proofs: Classical propositional calculus
    Hyland, M
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2004, 3210 : 6 - 21
12345