Banca de DEFESA: BRUNO FRANCISCO XAVIER

Uma banca de DEFESA de DOUTORADO foi cadastrada pelo programa.
STUDENT : BRUNO FRANCISCO XAVIER
DATE: 19/05/2023
TIME: 08:00
LOCAL: Google Meets
TITLE:

Linear logic as a framework


KEY WORDS:

Linear Logic; Framework; Cut elimination; Multimodality; Coq


PAGES: 173
BIG AREA: Ciências Exatas e da Terra
AREA: Ciência da Computação
SUBÁREA: Teoria da Computação
SPECIALTY: Lógicas e Semântica de Programas
SUMMARY:

This thesis investigates the analyticity of proof systems using Linear Logic (LL). Analyticity refers to the property that a proof of a formula F only uses subformulas of F. In sequent calculus, this property is typically established by showing that the cut rule is admissible, meaning that the introduction of the auxiliary lemma A in the reasoning “if A follows from B and C follows from A, then C follows from B” can be eliminated. However, cut-elimination is a complex process that involves multiple proof transformations and requires the use of (semi-)automatic procedures to prevent mistakes. LL is a powerful tool for studying the analyticity of proof systems due to its resource-conscious nature, the focused system, and its cut-elimination theorem. Previous works by Miller and Pimentel have used LL as a logical framework for establishing sufficient conditions for cut-elimination of object logics (OL). However, many logical systems cannot be adequately encoded in LL, particularly sequent systems for modal logics. In this thesis, we utilize a linear nested sequent (LNS) presentation of a variant of LL with subexponentials (MMLL) and demonstrate that it is possible to establish a cut-elimination criterion for a broader class of logical systems. This includes LNS proof systems for classical and substructural multimodal logics, as well as the LNS system for intuitionistic logic. Additionally, we present an in-depth study of the cut-elimination procedure for LL. Specifically, we propose a set of cut rules for focused systems for LL, a variant of LL with subexponentials (SELL) and MMLL. Our research demonstrates that these cut rules are sufficient for directly establishing the admissibility of cut within the focused systems. We formalize our results in Coq, a formal proof assistant, providing procedures for verifying cut-admissibility of several logical systems that are commonly used in philosophy, mathematics, and computer science.


COMMITTEE MEMBERS:
Presidente - 2114893 - CARLOS ALBERTO OLARTE VEGA
Interno - 1345816 - REGIVAN HUGO NUNES SANTIAGO
Interno - 1495704 - UMBERTO SOUZA DA COSTA
Externa à Instituição - ELAINE GOUVEA PIMENTEL - UCL
Externa à Instituição - GISELLE MACHADO NOGUEIRA REIS
Notícia cadastrada em: 11/05/2023 11:29
SIGAA | Superintendência de Tecnologia da Informação - (84) 3342 2210 | Copyright © 2006-2024 - UFRN - sigaa05-producao.info.ufrn.br.sigaa05-producao