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 条
  • [41] Termination Proofs for Linear Simple Loops
    Chen, Hong Yi
    Flur, Shaked
    Mukhopadhyay, Supratik
    STATIC ANALYSIS, SAS 2012, 2012, 7460 : 422 - 438
  • [42] Surface Proofs for Nonsymmetric Linear Logic
    Dunn, Lawrence
    Vicary, Jamie
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (238): : 33 - 43
  • [43] On proofs of Minkowskis clauses on linear forms
    von Neumann, J
    MATHEMATISCHE ZEITSCHRIFT, 1929, 30 : 1 - 2
  • [44] Proofs of God: Classical Arguments from Tertullian to Barth
    Siniscalchi, Glenn B.
    REVIEW OF METAPHYSICS, 2019, 72 (03): : 606 - 607
  • [45] Zero-Knowledge Proofs for Classical Planning Problems
    Correa, Augusto B.
    Buchner, Clemens
    Christen, Remo
    THIRTY-SEVENTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, VOL 37 NO 10, 2023, : 11955 - 11962
  • [46] INDEPENDENCE PROOFS IN NON-CLASSICAL SET THEORIES
    Tarafder, Sourav
    Venturi, Giorgio
    REVIEW OF SYMBOLIC LOGIC, 2023, 16 (04): : 979 - 1010
  • [47] ELEMENTARY PROOFS OF SOME CLASSICAL STABILITY-CRITERIA
    CHAPELLAT, H
    MANSOUR, M
    BHATTACHARYYA, SP
    IEEE TRANSACTIONS ON EDUCATION, 1990, 33 (03) : 232 - 239
  • [48] Proofs of some classical theorems in minimal surface theory
    Meeks, WH
    INDIANA UNIVERSITY MATHEMATICS JOURNAL, 2005, 54 (04) : 1031 - 1045
  • [49] MEANING AND PROOFS - CONFLICT BETWEEN CLASSICAL AND INTUITIONISTIC LOGIC
    PRAWITZ, D
    THEORIA, 1977, 43 : 2 - 40
  • [50] Proofs of God: Classical Arguments from Tertullian to Barth
    Schenkewitz, Kyle A.
    NEWMAN STUDIES JOURNAL, 2018, 15 (02) : 79 - 80
12345