The decidability of the intensional fragment of classical linear logic

• 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.