Banca de DEFESA: BRUNO FRANCISCO XAVIER

Uma banca de DEFESA de DOUTORADO foi cadastrada pelo programa.
DISCENTE : BRUNO FRANCISCO XAVIER
DATA : 19/05/2023
HORA: 08:00
LOCAL: Google Meets
TÍTULO:

Lógica linear como framework lógico 

PALAVRAS-CHAVES:

Lógica Linear; Framework; Eliminação do Corte; Multimodalidade; Coq

PÁGINAS: 173
RESUMO:

Esta tese investiga a analiticidade de sistemas de prova por meio da Lógica Linear (LL). A analiticidade é a propriedade de que uma prova de uma fórmula F usa apenas subfórmulas de F. No cálculo de sequentes, essa propriedade é geralmente estabelecida mostrando que a regra de corte é admissível, o que significa que a introdução do lema auxiliar A na proposição “se A segue de B e C segue de A, então C segue de B” pode ser eliminada. No entanto, a eliminação de corte é um processo complexo que envolve múltiplas transformações de prova e requer o uso de procedimentos (semi-)automáticos para evitar erros. LL é uma ferramenta poderosa para estudar a analiticidade de sistemas de prova devido à sua natureza orientada à recursos, ao sistema focado e seu teorema de eliminação de corte. Trabalhos anteriores de Miller e Pimentel utilizaram LL como um framework lógico para estabelecer condições suficientes para a eliminação de corte de lógicas objeto. No entanto, muitos sistemas lógicos não podem ser adequadamente codificados em LL, particularmente sistemas de sequentes para lógicas modais. Nesta tese, propomos um sistema de sequentes aninhados linearmente (LNS, do inglês linear nested sequents) de uma variante de LL com subexponenciais (MMLL) e demonstramos que é possível estabelecer um critério de eliminação de corte para uma classe mais ampla de sistemas lógicos. Isso inclui sistemas de prova LNS para lógicas multimodais clássicas e subestruturais, bem como o sistema LNS para lógica intuicionista. Além disso, apresentamos um estudo detalhado do procedimento de eliminação de corte para LL. Especificamente, propomos um conjunto de regras de corte para sistemas focados em LL, uma variante de LL com subexponenciais (SELL) e MMLL. Nossa pesquisa demonstrou que essas regras de corte são suficientes para estabelecer diretamente a admissibilidade de corte nos sistemas focados. Formalizamos nossos resultados em Coq, um assistente de prova formal, fornecendo procedimentos para verificar a eliminação de corte de vários sistemas lógicos que são comumente usados em filosofia, matemática e ciência da computação.

MEMBROS DA BANCA:
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