Banca de DEFESA: LAURA FERNANDES DELL ORTO

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
DISCENTE : LAURA FERNANDES DELL ORTO
DATA : 15/02/2017
HORA: 09:00
LOCAL: Sala de Seminários do DMAT
TÍTULO:

A study of Linear Logic with Subexponentials


PALAVRAS-CHAVES:

Mathematical Logic, Proof Theory, Cut-Elimination, Linear Logic, Linear Logic with Subexponenciais


PÁGINAS: 104
GRANDE ÁREA: Ciências Exatas e da Terra
ÁREA: Matemática
SUBÁREA: Matemática Aplicada
RESUMO:

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.


MEMBROS DA BANCA:
Presidente - 2114893 - CARLOS ALBERTO OLARTE VEGA
Interno - 1143603 - ELAINE GOUVEA PIMENTEL
Externo à Instituição - MÁRIO SÉRGIO FERREIRA ALVIM - UFMG
Notícia cadastrada em: 10/02/2017 11:00
SIGAA | Superintendência de Tecnologia da Informação - (84) 3342 2210 | Copyright © 2006-2024 - UFRN - sigaa05-producao.info.ufrn.br.sigaa05-producao