Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2017-04-03T22:46:24Z No. of bitstreams: 1 LauraFernandesDellOrto_DISSERT.pdf: 866111 bytes, checksum: 0ef11e74d1508214463b993885352d6c (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2017-04-11T20:56:41Z (GMT) No. of bitstreams: 1 LauraFernandesDellOrto_DISSERT.pdf: 866111 bytes, checksum: 0ef11e74d1508214463b993885352d6c (MD5) / Made available in DSpace on 2017-04-11T20:56:41Z (GMT). No. of bitstreams: 1 LauraFernandesDellOrto_DISSERT.pdf: 866111 bytes, checksum: 0ef11e74d1508214463b993885352d6c (MD5) Previous issue date: 2017-02-15 / Em L?gica Cl?ssica, podemos utilizar as hip?teses um n?mero indeterminado de vezes. Por exemplo, a prova de um teorema pode fazer uso do mesmo lema v?rias vezes. Por?m, em sistemas f?sicos, qu?micos e computacionais a situa??o ? diferente: um recurso n?o pode ser reutilizado ap?s ser consumido em uma a??o. Em L?gica Linear, f?rmulas s?o vistas como recursos a serem utilizados durante a prova. ? essa no??o de recursos que faz a L?gica Linear ser interessante para a modelagem de sistemas. Para tanto, a L?gica Linear controla o uso da contra??o e do enfraquecimento atrav?s dos exponenciais ! e ?. Este trabalho tem como objetivo fazer um estudo sobre a L?gica Linear com Subexponenciais (SELL), que ? um refinamento da L?gica Linear. Em SELL, os exponenciais da L?gica Linear possuem ?ndices, isto ?, ! e ? ser?o substitu?dos por !i e ?i, onde ?i? ? um ?ndice. Um dos pontos fundamentais de Teoria da Prova ? a prova da Elimina??o do Corte, que neste trabalho ? demonstrada tanto para L?gica Linear como para SELL, onde apresentamos detalhes que normalmente s?o omitidos. A partir do teorema de Elimina??o do Corte, podemos concluir a consist?ncia do sistema (para as l?gicas que estamos utilizando) e outros resultados como a propriedade de subf?rmula. O trabalho inicia-se com um cap?tulo de Teoria da Prova, e em seguida se faz uma exposi??o sobre a L?gica Linear. Assim, com essas bases, apresenta-se a L?gica Linear com Subexponenciais. SELL tem sido utilizada, por exemplo, na especifica??o e verifica??o de diferentes sistemas tais como sistemas bioqu?micos, sistemas de intera??o multim?dia e, em geral, em sistemas concorrentes com modalidades temporais, espaciais e epist?micas. Com essa base te?rica bastante clara, apresenta-se a especifica??o de um sistema bioqu?mico utilizando SELL. Al?m disso, apresentamos v?rias inst?ncias de SELL que tem interpreta??es interessantes do ponto de vista computacional. / 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.