Banca de QUALIFICAÇÃO: BRUNO FRANCISCO XAVIER

Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
DISCENTE : BRUNO FRANCISCO XAVIER
DATA : 25/11/2016
HORA: 09:00
LOCAL: Sala de seminários da Matemática CCET
TÍTULO:
Formalização de Lógica Linear em Coq.

PALAVRAS-CHAVES:
logica linear, coq, eliminação do corte

PÁGINAS: 70
RESUMO:
Em teoria da prova, o teorema da eliminação do corte (ou Hauptsatz, que significa resultado principal) é de 
suma importância, uma vez que implica a consistência e a propriedade subfórmula para um dado sistema.
Ele assinala que qualquer prova em cálculo de sequentes que faz uso da regra do corte pode ser substituida
por outra que não a utiliza. A prova procede por indução na ordem lexicográfica (peso da fórmula, altura do
corte) e gera múltiplos casos quando a fórmula de corte é ou não principal. De forma geral, deve-se
considerar a última regra aplicada nas duas premissas imediatamente depois de aplicar a regra do corte, o
que gera um número considerável de situações. Por essa razão, a demonstração poderia ser propensa a
erros na hipótese de recorremos a uma prova informal.  A lógica linear (LL) é uma das lógicas subestruturais
mais significativas e a regra do corte é admissível no seu cálculo de sequentes. Ela é um refinamento do
modelo clássico e intuicionista. Sendo uma lógica sensível ao uso de recursos, a LL tem sido amplamente
utilizada na especificação e verificação de sistemas computacionais. À vista disso, se torna relevante sua
abordagem neste trabalho. Nesta dissertação, formalizamos, em Coq, três cálculos de sequentes para a lógica
 linear e provamos que são equivalentes. Além disso, provamos metateoremas tais como admissibilidade da
regra do corte, generalização das regras para axioma inicial, bang e copy e invertibilidade das regras para os
 conectivos par, bot, with e quest. No tocante a invertibilidade, demonstramos uma versão por indução sobre
a altura da derivação e outra com aplicação da regra do corte, o que nos possibilitou conferir que, em um
sistema que satisfaz Hauptsatz, a regra do corte simplifica bastante as provas em seu cálculo de sequentes.
Com a finalidade de atenuar o número dos diversos casos, desenvolvemos várias táticas em Coq que nos
permite realizar operações semiautomáticas.

MEMBROS DA BANCA:
Presidente - 2114893 - CARLOS ALBERTO OLARTE VEGA
Interno - 1143603 - ELAINE GOUVEA PIMENTEL
Externo à Instituição - MÁRIO SÉRGIO ALVIM - UFMG
Notícia cadastrada em: 26/10/2016 17:04
SIGAA | Superintendência de Tecnologia da Informação - | | Copyright © 2006-2023 - UFRN - sigaa06-producao.info.ufrn.br.sigaa06-producao