Um estudo de lógica linear com subexponenciais

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...

ver descrição completa

Na minha lista:
Detalhes bibliográficos
Autor principal: Orto, Laura Fernandes Dell
Outros Autores: Vega, Carlos Alberto Olarte
Formato: Dissertação
Idioma:por
Publicado em: Brasil
Assuntos:
Lógica Matemática
Teoria da prova
Eliminação do corte
Lógica linear
Lógica linear com subexponenciais
CNPQ::CIENCIAS EXATAS E DA TERRA::MATEMATICA: MATEMÁTICA APLICADA E ESTATÍSTICA
Endereço do item:https://repositorio.ufrn.br/jspui/handle/123456789/22623
Tags: Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
id ri-123456789-22623
record_format dspace
institution Repositório Institucional
collection RI - UFRN
language por
topic Lógica Matemática
Teoria da prova
Eliminação do corte
Lógica linear
Lógica linear com subexponenciais
CNPQ::CIENCIAS EXATAS E DA TERRA::MATEMATICA: MATEMÁTICA APLICADA E ESTATÍSTICA
spellingShingle Lógica Matemática
Teoria da prova
Eliminação do corte
Lógica linear
Lógica linear com subexponenciais
CNPQ::CIENCIAS EXATAS E DA TERRA::MATEMATICA: MATEMÁTICA APLICADA E ESTATÍSTICA
Orto, Laura Fernandes Dell
Um estudo de lógica linear com subexponenciais
description 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.
author2 Vega, Carlos Alberto Olarte
author_facet Vega, Carlos Alberto Olarte
Orto, Laura Fernandes Dell
format masterThesis
author Orto, Laura Fernandes Dell
author_sort Orto, Laura Fernandes Dell
title Um estudo de lógica linear com subexponenciais
title_short Um estudo de lógica linear com subexponenciais
title_full Um estudo de lógica linear com subexponenciais
title_fullStr Um estudo de lógica linear com subexponenciais
title_full_unstemmed Um estudo de lógica linear com subexponenciais
title_sort um estudo de lógica linear com subexponenciais
publisher Brasil
publishDate 2017
url https://repositorio.ufrn.br/jspui/handle/123456789/22623
work_keys_str_mv AT ortolaurafernandesdell umestudodelogicalinearcomsubexponenciais
AT ortolaurafernandesdell astudyoflinearlogicwithsubexponentials
_version_ 1773967562900504576
spelling ri-123456789-226232017-11-04T10:02:32Z Um estudo de lógica linear com subexponenciais A study of linear logic with subexponentials Orto, Laura Fernandes Dell Vega, Carlos Alberto Olarte http://lattes.cnpq.br/7762552636864447 http://lattes.cnpq.br/1198550954813139 Pimentel, Elaine Gouvea http://lattes.cnpq.br/3298246411086415 Alvim, Mário Sérgio Ferreira http://lattes.cnpq.br/1397639761790594 Pimentel, Elaine Gouvea http://lattes.cnpq.br/3298246411086415 Lógica Matemática Teoria da prova Eliminação do corte Lógica linear Lógica linear com subexponenciais CNPQ::CIENCIAS EXATAS E DA TERRA::MATEMATICA: MATEMÁTICA APLICADA E ESTATÍSTICA 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. 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. 2017-04-11T20:56:41Z 2017-04-11T20:56:41Z 2017-02-15 masterThesis ORTO, Laura Fernandes Dell. Um estudo de lógica linear com subexponenciais. 2017. 109f. Dissertação (Mestrado em Matemática Aplicada e Estatística) - Centro de Ciências Exatas e da Terra, Universidade Federal do Rio Grande do Norte, Natal, 2017. https://repositorio.ufrn.br/jspui/handle/123456789/22623 por Acesso Aberto application/pdf Brasil UFRN PROGRAMA DE PÓS-GRADUAÇÃO EM MATEMÁTICA APLICADA E ESTATÍSTICA

Registros relacionados