A unified view of modal and substructural logics

  (Elaine Pimentel)


It is well known that context dependent logical rules can be hard to
both, implement and reason about. This is one of the reasons for the
quest for better behaved logical systems. In the case of modalities,
local rules can be, in general, described using generalizations of
sequent calculus systems.
In this work, we propose a general framework for describing systems
based on multiplicative additive linear logic plus simply dependent
multimodalities. This class of systems includes linear logic with
subexponentials (SELL). The chosen approach is linear nested sequents
(LNS).
It turns out that LNS systems can be adequately encoded into (plain)
linear logic, showing that LL is, in fact an ``universal framework''
for the specification of logical systems.
From the theoretical point of view, our results show that (1) logics
such as SELL, that were thought to be more expressive than LL, are, in
fact, equally expressive; and (2) it is possible to give an uniform
presentation to linear logics featuring different axioms of
modalities. From the practical point of view, our results: (3) lead to
a generic way of building theorem provers for different logics, all of
them based on the same grounds; and (4) allow for the use of the same
logical framework for reasoning about all such logical systems.

This is a joint work with Bjorn Lellmann and Carlos Olarte.