Linear Logic Properly Displayed
Greco, Palmigiano · math.LO,cs.LO,math.CT · 2016-11-13 · 原文
We introduce proper display calculi for intuitionistic, bi-intuitionistic and classical linear logics with exponentials, which are sound, complete, conservative, and enjoy cut-elimination and subformula property. Based on the same design, we introduce a variant of Lambek calculus with exponentials, aimed at capturing the controlled application of exchange and associativity. Properness (i.e. closure under uniform substitution of all parametric parts in rules) is the main interest and added value of the present proposal, and allows for the smoothest proof of cut-elimination. Our proposal builds on an algebraic and order-theoretic analysis of linear logic, and applies the guidelines of the multi-type methodology in the design of display calculi.
讲义
讲义·推断 依据「原文」自动生成的结构化摘要（推断），非原文表述；以原文为准。
1. 人话版
We introduce proper display calculi for intuitionistic, bi-intuitionistic and classical linear logics with exponentials, which are sound, complete, conservative, and enjoy cut-elimination and subformula property.
Based on the same design, we introduce a variant of Lambek calculus with exponentials, aimed at capturing the controlled application of exchange and associativity.
2. 领域脉络
本文类目：math.LO、cs.LO、math.CT，属于其所在研究脉络的最新进展。
3. 机制拆解
Properness (i.e.
closure under uniform substitution of all parametric parts in rules) is the main interest and added value of the present proposal, and allows for the smoothest proof of cut-elimination.
Our proposal builds on an algebraic and order-theoretic analysis of linear logic, and applies the guidelines of the multi-type methodology in the design of display calculi.
4. 证据与数字
摘要未给出量化结果——留意原文的实验与数据。
5. 反例与边界
摘要未声明局限与反例——这是需要警惕的信号，精读时先问边界。
6. 跨领域连接与意外收获
横跨 3 个类目（math.LO、cs.LO、math.CT），关注其在你兴趣板块间的迁移面。
7. 可复用方法
把本文机制与你手头项目对照，找一个两周内能验证的最小实验。
8. 术语表
精读时把不熟的术语记入此处，作为下次回忆的锚点。