Um estudo de lógica linear com subexponenciais

Abstract

In Classical Logic, we can use a given hypothesis an indefinite number of times. For example, the proof of a theorem may use the same lemma several times. However, in physical, chemical and computational systems, the situation is different: a resource cannot be reused after being consumed in one action. In Linear Logic, formulas are seen as resources to be used during a proof. This feature makes Linear Logic an interesting formalism for the specification and verification of such systems. Linear Logic controls the rules of contraction and weakening through the exponentials ! and ?. This work aims to study Linear Logic with subexponentials (SELL), which is a refinement of Linear Logic. In SELL, the exponentials of Linear Logic are decorated with indexes, i.e., ! and ? are replaced with !i and ?i, where “i” is an index. One of the main results in Proof Theory is the Cut-Elimination theorem. In this work we demonstrate that theorem for both Linear Logic and SELL, where we present details that are usually omitted in the literature. From the Cut-Elimination Theorem, we can show, as a corollary, the consistency of the system (for the logics considered here) and other results as the subformula property. This work begins with an introduction to Proof Theory and then, it presents Linear Logic. On these bases, we present Linear Logic with subexponentials. SELL has been used, for example, in the specification and verification of various systems such as biochemical systems, multimedia interaction systems and, in general, concurrent systems with temporal, spatial and epistemic modalities. Using the theory of SELL, we show the specification of a biochemical system. Moreover, we present several instances of SELL that have interesting interpretations from a computational point of view.