Banca de QUALIFICAÇÃO: BRUNO FRANCISCO XAVIER

Uma banca de QUALIFICAÇÃO de DOUTORADO foi cadastrada pelo programa.
DISCENTE : BRUNO FRANCISCO XAVIER
DATA : 12/04/2022
HORA: 14: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: 138
RESUMO:

O uso da lógica linear como framework lógico consiste em: (1) incorporar sequentes de uma dada lógica objeto usando dois predicados na lógica linear que diferenciam fórmulas do lado esquerdo das fórmulas do lado direito; e (2) traduzir as regras do cálculo de sequentes da lógica objeto como teorias (cláusulas) da lógica linear. Se o conjunto de teorias possui certas características, podemos estabelecer resultados interessantes, como por exemplo a admissibilidade do corte, sem que seja necessário uma prova direta na lógica objeto. Usar a lógica linear como framework para raciocinar sobre diversos sistemas lógicos, em particular sistemas modais, e estabelecer traduções adequadas que obedeçam as características necessárias para concluir a admissibilidade do corte desses sistemas é o objetivo deste trabalho. Além de formalizar todos os resultados em um provador semiautomático de teoremas. Trata-se de uma pesquisa aplicada, de cunho descritivo, mediante revisão de estudos do uso da lógica linear como framework e extensão do framework. Destaca-se novos resultados de eliminação do corte para a lógica linear diretamente no sistema focado com e sem subexponeciais e construção de um framework baseado na lógica linear com multimodalidades mecanizados no provador de teoremas Coq.

MEMBROS DA BANCA:
Interno - 2114893 - CARLOS ALBERTO OLARTE VEGA
Interna - 1143603 - ELAINE GOUVEA PIMENTEL
Interno - 1345816 - REGIVAN HUGO NUNES SANTIAGO
Externa à Instituição - GISELLE MACHADO NOGUEIRA REIS