The decidability of the intensional fragment of classical linear logic

摘要

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. (C) 2015 Elsevier B.V. All rights reserved.