A Linear Proof Language for Second-Order Intuitionistic Linear Logic

被引：0

作者：

Diaz-Caro, Alejandro ^{[1
,2
,3
]}

Dowek, Gilles ^{[4
]}

Ivnisky, Malena ^{[2
,3
,5
]}

Malherbe, Octavio ^{[6
]}

机构：

[1] Univ Nacl Quilmes, DCyT, Bernal, Pba, Argentina

[2] Univ Buenos Aires, FCEyN, DC, Buenos Aires, DF, Argentina

[3] Univ Buenos Aires, CONICET, ICC, Buenos Aires, DF, Argentina

[4] ENS Paris Saclay, LMF, INRIA, Gif Sur Yvette, France

[5] Univ La Republ MEC, PEDECIBA, Montevideo, Uruguay

[6] Univ La Republ, FIng, IMERL, Montevideo, Uruguay

来源：

LOGIC, LANGUAGE, INFORMATION, AND COMPUTATION, WOLLIC 2024 | 2024年 / 14672卷

关键词：

Proof theory; Lambda calculus; Linear logic; Polymorphism;

D O I：

10.1007/978-3-031-62687-6_2

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We present a polymorphic linear lambda-calculus as a proof language for second-order intuitionistic linear logic. The calculus includes addition and scalar multiplication, enabling the proof of a linearity result at the syntactic level.

引用

页码：18 / 35

页数：18

共 50 条

[1] Decision problems for second-order linear logic
Lincoln, PD
Scedrov, A
Shankar, N
[J]. LOGIC AND SCIENTIFIC METHODS: VOLUME ONE OF THE TENTH INTERNATIONAL CONGRESS OF LOGIC, METHODOLOGY AND PHILOSOPHY OF SCIENCE, FLORENCE, AUGUST 1995, 1997, 259 : 127 - 143
[2] Linear delay enumeration and monadic second-order logic
Courcelle, Bruno
[J]. DISCRETE APPLIED MATHEMATICS, 2009, 157 (12) : 2675 - 2700
[3] Monadic second-order logic and linear orderings of finite structures
Courcelle, B
[J]. COMPUTER SCIENCE LOGIC, 1995, 933 : 163 - 176
[4] Second-order linear reasoning mechanisms for description logic ΕL
[J]. Chen, Guang-Xi (chgx@guet.edu.cn), 2017, Chinese Academy of Sciences (28):
[5] A PSPACE-complete fragment of second-order linear logic
Perrier, G
[J]. THEORETICAL COMPUTER SCIENCE, 1999, 224 (1-2) : 267 - 289
[6] Completeness of Second-Order Intuitionistic Propositional Logic with Respect to Phase Semantics for Proof-Terms
Yuta Takahashi
Ryo Takemura
[J]. Journal of Philosophical Logic, 2019, 48 : 553 - 570
[7] Completeness of Second-Order Intuitionistic Propositional Logic with Respect to Phase Semantics for Proof-Terms
Takahashi, Yuta
Takemura, Ryo
[J]. JOURNAL OF PHILOSOPHICAL LOGIC, 2019, 48 (03) : 553 - 570
[8] Expressing Second-order Sentences in Intuitionistic Dependence Logic
Yang, Fan
[J]. STUDIA LOGICA, 2013, 101 (02) : 323 - 342
[9] Expressing Second-order Sentences in Intuitionistic Dependence Logic
Fan Yang
[J]. Studia Logica, 2013, 101 : 323 - 342
[10] LINEAR ITERATION OF SECOND-ORDER
DHOMBRES, J
[J]. COMPTES RENDUS HEBDOMADAIRES DES SEANCES DE L ACADEMIE DES SCIENCES SERIE A, 1975, 280 (05): : 275 - 277

← 1 2 3 4 5 →