Banca de DEFESA: BRUNO FRANCISCO XAVIER

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
DISCENTE : BRUNO FRANCISCO XAVIER
DATA : 15/02/2017
HORA: 08:00
LOCAL: Sala de seminários da Matemática CCET
TÍTULO:

Formalização da Lógica Linear em Coq

PALAVRAS-CHAVES:

lógica 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, em geral, 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 substituída 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 que pode ser considerada um refinamento das lógicas clássica e intuicionista e o teorema da eliminação do corte é válido para ela. Sendo uma lógica sensível ao uso de recursos, 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, bottom, with e quest. Com relação à invertibilidade, a demonstração foi elaborada de duas maneiras: 1) por indução sobre a altura da derivação e 2) utilizando a regra do corte. A diferença das duas provas mostra que, em um sistema que satisfaz Hauptsatz, a regra do corte simplifica bastante as provas em seu cálculo de sequentes. Finalmente, com a finalidade de atenuar o número dos diversos casos, neste trabalho desenvolvemos várias táticas em Coq que nos permitiram automatizar parte das provas.

MEMBROS DA BANCA:
Presidente - 2114893 - CARLOS ALBERTO OLARTE VEGA
Interno - 1143603 - ELAINE GOUVEA PIMENTEL
Externo à Instituição - MÁRIO SÉRGIO FERREIRA ALVIM - UFMG