Intuitionistic linear logic and partial correctness

被引：1

作者：

Kozen, D ^{[1
]}

Tiuryn, J ^{[1
]}

机构：

[1] Cornell Univ, Ithaca, NY 14853 USA

来源：

16TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS | 2001年

关键词：

D O I：

10.1109/LICS.2001.932502

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We formulate a Gentzen-style sequent calculus for partial correctness that subsumes propositional Hoare Logic. The system is a noncommutative intuitionistic Linear Logic. We prove soundness and completeness over relational and trace models. As a corollary we obtain a complete sequent calculus for inclusion and equivalence of regular expressions.

引用

页码：259 / 268

页数：10

共 50 条

[1] Linear logic and intuitionistic logic
Okada, M
[J]. REVUE INTERNATIONALE DE PHILOSOPHIE, 2004, 58 (230) : 449 - 481
[2] Skolemisation for Intuitionistic Linear Logic
Bruni, Alessandro
Ritter, Eike
Schurmann, Carsten
[J]. AUTOMATED REASONING, IJCAR 2024, PT II, 2024, 14740 : 61 - 77
[3] NONCOMMUTATIVE INTUITIONISTIC LINEAR LOGIC
ABRUSCI, VM
[J]. ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1990, 36 (04): : 297 - 318
[4] LOGIC PROGRAMMING IN A FRAGMENT OF INTUITIONISTIC LINEAR LOGIC
HODAS, JS
MILLER, D
[J]. INFORMATION AND COMPUTATION, 1994, 110 (02) : 327 - 365
[5] NONMODAL CLASSICAL LINEAR PREDICATE LOGIC IS A FRAGMENT OF INTUITIONISTIC LINEAR LOGIC
DOSEN, K
[J]. THEORETICAL COMPUTER SCIENCE, 1992, 102 (01) : 207 - 214
[6] The ILLTP Library for Intuitionistic Linear Logic
Olarte, Carlos
de Paiva, Valeria
Pimentel, Elaine
Reis, Giselle
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2019, (292): : 118 - 132
[7] FUNCTIONAL INTERPRETATIONS OF INTUITIONISTIC LINEAR LOGIC
Ferreira, Gilda
Oliva, Paulo
[J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2011, 7 (01)
[8] Lambda calculus and intuitionistic linear logic
Rocca S.R.D.
Roversi L.
[J]. Studia Logica, 1997, 59 (3) : 417 - 448
[9] Normal deduction in the intuitionistic linear logic
G. Mints
[J]. Archive for Mathematical Logic, 1998, 37 : 415 - 425
[10] NATURAL DEDUCTION FOR INTUITIONISTIC LINEAR LOGIC
TROELSTRA, AS
[J]. ANNALS OF PURE AND APPLIED LOGIC, 1995, 73 (01) : 79 - 108

← 1 2 3 4 5 →