Banca de QUALIFICAÇÃO: LAURA FERNANDES DELL ORTO

Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
DISCENTE : LAURA FERNANDES DELL ORTO
DATA : 25/11/2016
HORA: 08:00
LOCAL: Sala de seminários da Matemática CCET
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: 85
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 and computer 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 the 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 the Cut Elimination theorem for both Linear Logic and 
SELL. From the Cut-Elimination Theorem, we can show, as a corollary,  the consistency of the system and 
other results as the subformula property. This work begins with a brief history of Mathematical Logic and then, 
it delves into Proof Theory and 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 plan to specify a real (physical)
 or a mathematical (abstract) 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