Proof nets sequentialisation in multiplicative linear logic

被引：3

作者：

Di Giamberardino, Paolo ^{[1
]}

Faggian, Claudia ^{[2
]}

机构：

[1] Univ Roma Tre, Inst Math Luminy, Dipartimento Filosofia, Rome, Italy

[2] Preuves Programmes & Syst, Paris 7, France

来源：

ANNALS OF PURE AND APPLIED LOGIC | 2008年 / 155卷 / 03期

关键词：

Linear logic; Proof nets; Sequentialization;

D O I：

10.1016/j.apal.2008.04.002

中图分类号：

O29 [应用数学];

学科分类号：

070104 ;

摘要：

We provide an alternative proof of the sequentialisation theorem for proof nets of multiplicative linear logic. Namely, we show how a proof net can be transformed into a sequent calculus proof simply by properly adding to it some special edges, called sequential edges, which express the sequentiality constraints given by sequent calculus. (c) 2008 Elsevier B.V. All rights reserved.

引用

页码：173 / 182

页数：10

共 10 条

[1] SEQUENT RECONSTRUCTION IN LLM - A SWEEPLINE PROOF
BANACH, R
[J]. ANNALS OF PURE AND APPLIED LOGIC, 1995, 73 (03) : 277 - 295
[2] Bellin G., 1995, ADV LINEAR LOGIC
[3] Curien P.-L., 2005, LNCS
[4] CURIEN PL, APPROACH INNOCENT ST
[5] Danos Vincent, 1990, Phd thesis
[6] DIGIAMBERARDINO P, 2006, LECT NOTES COMPUTER
[7] GIRARD JV, 1996, LOGIC ALGEBRA
[8] LINEAR LOGIC
GIRARD, JY
[J]. THEORETICAL COMPUTER SCIENCE, 1987, 50 (01) : 1 - 102
[9] GIRARD JY, 1991, NUOVI PROBLEMI LOGIC
[10] HUGHES D, 2003, P LICS 03 IEEE

← 1 →