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:
Formalizing Linear Logic in Coq

PALAVRAS-CHAVES:
linear logic, coq, cut-elimination

PÁGINAS: 70
GRANDE ÁREA: Ciências Exatas e da Terra
ÁREA: Matemática
SUBÁREA: Matemática Aplicada
RESUMO:
In proof  theory, the cut-elimination theorem (or Hauptsatz, which means main result) is of paramount 
importance since it implies the consistency and the subformula property for the given system. This theorem
states that  any proof in the sequent calculus that makes use of the cut rule can be replaced by other that does
 not make use of it. The proof of cut-elimination proceeds by induction on lexicographical order (formula
weight, rule cut height) and generates multiple cases,  considering for instance,  when the formula generated
by the cut rule is, or is not, principal. In general, one must consider the last rule applied in the two premises
 immediately after applying the cut rule (seeing the proof bottom-up), which generates a considerable amount
 of cases. For this reason, the proof of cut-elimination could be error prone if we use an informal proof. Linear
 Logic (LL) is one of the most significant substructural logics and the cut rule is admissible in its sequent
calculus. LL is a refinement of classical and intuitionistic logics. As a resource sensible logic, LL has been widely
 used in the specification and verification of computer systems. In view of this, it becomes relevant the study
 of this logic in this work. In this dissertation we formalize three sequent calculus for linear logic in Coq and
prove all of them equivalent. Additionally, we formalized meta-theorems such as admissibility of cut,
generalization of initial rule, bang and copy and invertibility of the rules for the connectives par, bot, with and
quest. Regarding the invertibility, we demonstrate this theorem in two different ways: a version by induction
on the height of the derivation and by using the cut rule. This allows us to show how the cut rule greatly
simplifies the proofs in the sequent calculus. In order to mitigate the number of several cases in the proofs,
we develop several tactics in coq that allows us to perform semi-automatic operations.

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 - (84) 3342 2210 | Copyright © 2006-2024 - UFRN - sigaa04-producao.info.ufrn.br.sigaa04-producao