Formaliza??o da l?gica linear em Coq

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2017-04-03T22:46:23Z No. of bitstreams: 1 BrunoFranciscoXavier_DISSERT.pdf: 923146 bytes, checksum: c0238dcb8801e0f87397d8417f0eb689 (MD5)

Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2017-04-11T20:33:34Z (GMT) No. of bitstreams: 1 BrunoFranciscoXavier_DISSERT.pdf: 923146 bytes, checksum: c0238dcb8801e0f87397d8417f0eb689 (MD5)

Made available in DSpace on 2017-04-11T20:33:35Z (GMT). No. of bitstreams: 1 BrunoFranciscoXavier_DISSERT.pdf: 923146 bytes, checksum: c0238dcb8801e0f87397d8417f0eb689 (MD5) Previous issue date: 2017-02-15

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 na consist?ncia e na 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 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, 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, ! e copy e invertibilidade das regras para os conectivos ?, ?, & e ?. No tocante ? 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.

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 the lexicographical order (formula weight, 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). This thus generates a considerable amount of cases. For this reason, the proof of cut-elimination includes several cases and it 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 the classical and the intuitionistic model. 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 formalize 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 allow us to perform semi-automatic reasoning.