Decision Problems for Second-Order Linear Logic

1997 ◽  
pp. 127-143
Author(s):  
P. D. Lincoln ◽  
A. Scedrov ◽  
N. Shankar
Keyword(s):  
Linear Logic ◽  
Second Order ◽  
Decision Problems ◽  
Order Linear

The undecidability of second order linear logic without exponentials

1996 ◽  
Vol 61 (2) ◽  
pp. 541-548 ◽  
Author(s):  
Yves Lafont
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Linear Logic ◽  
Classical Case ◽  
Second Order ◽  
Order Linear ◽  
Phase Semantics ◽  
Counter Machines ◽  
Intuitionistic Linear Logic

AbstractRecently, Lincoln, Scedrov and Shankar showed that the multiplicative fragment of second order intuitionistic linear logic is undecidable, using an encoding of second order intuitionistic logic. Their argument applies to the multiplicative-additive fragment, but it does not work in the classical case, because second order classical logic is decidable. Here we show that the multiplicative-additive fragment of second order classical linear logic is also undecidable, using an encoding of two-counter machines originally due to Kanovich. The faithfulness of this encoding is proved by means of the phase semantics.

scholarly journals A PSPACE-complete fragment of second-order linear logic

1999 ◽  
Vol 224 (1-2) ◽  
pp. 267-289
Author(s):  
G. Perrier
Keyword(s):  
Linear Logic ◽  
Second Order ◽  
Order Linear

scholarly journals A phase semantics for polarized linear logic and second order conservativity

2010 ◽  
Vol 75 (1) ◽  
pp. 77-102 ◽  
Author(s):  
Masahiro Hamano ◽  
Ryo Takemura
Keyword(s):  
Topological Structure ◽  
Linear Logic ◽  
Second Order ◽  
Order Linear ◽  
First Order ◽  
Counter Model ◽  
Linear Fragment ◽  
Phase Semantics ◽  
Second Order Systems ◽  
Completeness Theorems

AbstractThis paper presents a polarized phase semantics, with respect to which the linear fragment of second order polarized linear logic of Laurent [15] is complete. This is done by adding a topological structure to Girard's phase semantics [9], The topological structure results naturally from the categorical construction developed by Hamano–Scott [12]. The polarity shifting operator ↓ (resp. ↑) is interpreted as an interior (resp. closure) operator in such a manner that positive (resp. negative) formulas correspond to open (resp. closed) facts. By accommodating the exponentials of linear logic, our model is extended to the polarized fragment of the second order linear logic. Strong forms of completeness theorems are given to yield cut-eliminations for the both second order systems. As an application of our semantics, the first order conservativity of linear logic is studied over its polarized fragment of Laurent [16]. Using a counter model construction, the extension of this conservativity is shown to fail into the second order, whose solution is posed as an open problem in [16]. After this negative result, a second order conservativity theorem is proved for an eta expanded fragment of the second order linear logic, which fragment retains a focalized sequent property of [3].

scholarly journals Strong normalization property for second order linear logic

2010 ◽  
Vol 411 (2) ◽  
pp. 410-444 ◽  
Author(s):  
Michele Pagani ◽  
Lorenzo Tortora de Falco
Keyword(s):  
Linear Logic ◽  
Second Order ◽  
Strong Normalization ◽  
Order Linear

Bases for Second Order Linear ODEs

2020 ◽  
Vol 127 (9) ◽  
pp. 849-849
Author(s):  
Peter McGrath
Keyword(s):  
Second Order ◽  
Order Linear ◽  
Linear Odes
Sign in / Sign up

Export Citation Format

Share Document