Polarized and focalized linear and classical proofs

被引：14
|
作者：
Laurent, O
Quatrini, M
de Falco, LT
机构：
[1] CNRS, Inst Math Luminy, Federat Rech, Unites Math Marseille, F-13288 Marseille, France
[2] Univ Mediterranee, F-13288 Marseille, France
[3] Univ Roma Tre, Dipartimento Filosofia, I-00146 Rome, Italy
来源：
ANNALS OF PURE AND APPLIED LOGIC | 2005年 / 134卷 / 2-3期
关键词：
classical logic; linear logic; cut-elimination; proof-nets; denotational semantics; polarization; focalization; reversion;
D O I：
10.1016/j.apal.2004.11.002
中图分类号：
O29 [应用数学];
学科分类号：
070104 ;
摘要：
We give the precise correspondence between polarized linear logic and polarized classical logic. The properties of focalization and reversion of linear proofs are at the heart of our analysis: we show that the tq-protocol of normalization for the classical systems LKpol eta and LKpol eta-p perfectly fits normalization of polarized proof-nets. Some more semantical considerations allow us to recover LC as a refinement of multiplicative LKpol eta. (c) 2005 Elsevier B.V. All rights reserved.
引用
收藏
页码：217 / 264
页数：48
相关论文
共 50 条
  • [21] CONSISTENCY PROOFS OF SUBSYSTEMS OF CLASSICAL ANALYSIS
    TAKEUTI, G
    ANNALS OF MATHEMATICS, 1967, 86 (02) : 299 - &
  • [22] Naming proofs in classical propositional logic
    Lamarche, F
    Strassburger, L
    TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS, 2005, 3461 : 246 - 261
  • [23] 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
  • [24] Equality of proofs for linear equality
    Dosen, Kosta
    Petric, Zoran
    ARCHIVE FOR MATHEMATICAL LOGIC, 2008, 47 (06) : 549 - 565
  • [25] Proofs as computations in linear logic
    Delzanno, G
    Martelli, M
    THEORETICAL COMPUTER SCIENCE, 2001, 258 (1-2) : 269 - 297
  • [26] Cyclic Proofs for Linear Temporal
    Kokkinis, Ioannis
    Studer, Thomas
    CONCEPTS OF PROOF IN MATHEMATICS, PHILOSOPHY, AND COMPUTER SCIENCE, 2016, 6 : 171 - 192
  • [27] Equality of proofs for linear equality
    Kosta Došen
    Zoran Petrić
    Archive for Mathematical Logic, 2008, 47 : 549 - 565
  • [28] CLASSICAL PROOFS AS PROGRAMS - HOW, WHAT AND WHY
    MURTHY, CR
    LECTURE NOTES IN COMPUTER SCIENCE, 1992, 613 : 71 - 88
  • [29] Classical proofs, typed processes, and intersection types
    Ghilezan, S
    Lescanne, P
    TYPES FOR PROOFS AND PROGRAMS, 2004, 3085 : 226 - 241
  • [30] Proofs and Countermodels in Non-Classical Logics
    Negri, Sara
    LOGICA UNIVERSALIS, 2014, 8 (01) : 25 - 60
12345