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 条
  • [31] Normal Natural Deduction Proofs (in classical logic)
    Wilfried Sieg
    John Byrnes
    Studia Logica, 1998, 60 (1) : 67 - 106
  • [32] Refined program extraction from classical proofs
    Berger, U
    Buchholz, W
    Schwichtenberg, H
    ANNALS OF PURE AND APPLIED LOGIC, 2002, 114 (1-3) : 3 - 25
  • [33] Abstract interpretation of proofs: Classical propositional calculus
    Hyland, M
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2004, 3210 : 6 - 21
  • [34] Practical Program Extraction from Classical Proofs
    Makarov, Yevgeniy
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 155 : 521 - 542
  • [35] SOME PROOFS OF THE CLASSICAL INTEGRAL HARDY INEQUALITY
    Muniru, Iddrisu Mohammed
    Adjei, Okpoti Christopher
    Alagbe, Gbolagade Kazeem
    KOREAN JOURNAL OF MATHEMATICS, 2014, 22 (03): : 407 - 417
  • [36] DENOTATIONS FOR CLASSICAL PROOFS - PRELIMINARY-RESULTS
    DEGROOTE, P
    LECTURE NOTES IN COMPUTER SCIENCE, 1992, 620 : 105 - 116
  • [37] On lengths of proofs in non-classical logics
    Hrubes, Pavel
    ANNALS OF PURE AND APPLIED LOGIC, 2009, 157 (2-3) : 194 - 205
  • [38] From proofs to focused proofs: A modular proof of focalization in linear logic
    Miller, Dale
    Saurin, Alexis
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2007, 4646 : 405 - +
  • [39] Termination proofs for linear simple loops
    Chen, Hong Yi
    Flur, Shaked
    Mukhopadhyay, Supratik
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2015, 17 (01) : 47 - 57
  • [40] Termination proofs for linear simple loops
    Hong Yi Chen
    Shaked Flur
    Supratik Mukhopadhyay
    International Journal on Software Tools for Technology Transfer, 2015, 17 : 47 - 57
12345