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: 09:00
LOCAL: Sala de seminários da Matemática CCET
TÍTULO:
 Formalization of 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 for any sequent that has a proof using the cut rule, it is possible to find a cut-free  proof for the same sequent. The proof of cut-elimination proceeds by induction on the lexicographical order (formula weight, cut height) and generates multiple cases, considering for instance, when the cut-formula is or 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). This generates a considerable amount of cases and then, the demonstration of this theorem could be error prone if we use an informal proof. Linear Logic (LL) is one of the most significant substructural logics and it allows for cut-free sequent calculi. LL is a resource sensible logic and 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 calculi for linear logic in Coq and prove all of them to be equivalent. Additionally, we formalize meta-theorems such as admissibility of cut, generalization of initial rule, bang and copy and invertibility of the rules for the connectives par, bottom, 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 reasoning.


MEMBROS DA BANCA:
Presidente - 2114893 - CARLOS ALBERTO OLARTE VEGA
Interno - 1143603 - ELAINE GOUVEA PIMENTEL
Externo à Instituição - MÁRIO SÉRGIO FERREIRA ALVIM - UFMG
Notícia cadastrada em: 31/01/2017 11:14
SIGAA | Superintendência de Tecnologia da Informação - (84) 3342 2210 | Copyright © 2006-2024 - UFRN - sigaa07-producao.info.ufrn.br.sigaa07-producao