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.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/22623 |
| Date | 15 February 2017 |
| Creators | Orto, Laura Fernandes Dell |
| Contributors | 70600793435, http://lattes.cnpq.br/1198550954813139, Alvim, M?rio S?rgio Ferreira, 05807109635, http://lattes.cnpq.br/1397639761790594, Pimentel, Elaine Gouvea, 84151781668, http://lattes.cnpq.br/3298246411086415, Pimentel, Elaine Gouvea, Vega, Carlos Alberto Olarte |
| Publisher | PROGRAMA DE P?S-GRADUA??O EM MATEM?TICA APLICADA E ESTAT?STICA, UFRN, Brasil |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0023 seconds