Article ID Journal Published Year Pages File Type
435811 Theoretical Computer Science 2015 17 Pages PDF
Abstract

•Intensional classical linear logic (MELL) is proved decidable.•Intensional interlinear logic (RLL) is proved decidable.•We adapt Kripke's method used to prove decidability for some relevance logics.•The semi-relevant RLL emerges as a logic superior to MELL in this context.•Triple and double inductive proofs of cut theorems are explained in some detail.

The intensional fragment of classical propositional linear logic combines modalities with contraction-free relevance logic — adding modalized versions of the thinning and contraction rules. This paper provides a proof of the decidability of this logic based on a sequent calculus formulation. Some related logics and some other fragments of linear logic are also shown decidable.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Authors
,