Formalização da lógica linear em Coq
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 repla...
Na minha lista:
Autor principal: | |
---|---|
Outros Autores: | |
Formato: | Dissertação |
Idioma: | por |
Publicado em: |
Brasil
|
Assuntos: | |
Endereço do item: | https://repositorio.ufrn.br/jspui/handle/123456789/22622 |
Tags: |
Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
|
id |
ri-123456789-22622 |
---|---|
record_format |
dspace |
institution |
Repositório Institucional |
collection |
RI - UFRN |
language |
por |
topic |
Lógica linear Coq Eliminação do corte CNPQ::CIENCIAS EXATAS E DA TERRA::MATEMATICA: MATEMÁTICA APLICADA E ESTATÍSTICA |
spellingShingle |
Lógica linear Coq Eliminação do corte CNPQ::CIENCIAS EXATAS E DA TERRA::MATEMATICA: MATEMÁTICA APLICADA E ESTATÍSTICA Xavier, Bruno Francisco Formalização da lógica linear em Coq |
description |
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. |
author2 |
Vega, Carlos Alberto Olarte |
author_facet |
Vega, Carlos Alberto Olarte Xavier, Bruno Francisco |
format |
masterThesis |
author |
Xavier, Bruno Francisco |
author_sort |
Xavier, Bruno Francisco |
title |
Formalização da lógica linear em Coq |
title_short |
Formalização da lógica linear em Coq |
title_full |
Formalização da lógica linear em Coq |
title_fullStr |
Formalização da lógica linear em Coq |
title_full_unstemmed |
Formalização da lógica linear em Coq |
title_sort |
formalização da lógica linear em coq |
publisher |
Brasil |
publishDate |
2017 |
url |
https://repositorio.ufrn.br/jspui/handle/123456789/22622 |
work_keys_str_mv |
AT xavierbrunofrancisco formalizacaodalogicalinearemcoq |
_version_ |
1773959718478282752 |
spelling |
ri-123456789-226222017-11-04T10:02:47Z Formalização da lógica linear em Coq Xavier, Bruno Francisco Vega, Carlos Alberto Olarte http://lattes.cnpq.br/0730802486637527 http://lattes.cnpq.br/1198550954813139 Pimentel, Elaine Gouvea http://lattes.cnpq.br/3298246411086415 Alvim, Mário Sérgio Ferreira http://lattes.cnpq.br/1397639761790594 Lógica linear Coq Eliminação do corte CNPQ::CIENCIAS EXATAS E DA TERRA::MATEMATICA: MATEMÁTICA APLICADA E ESTATÍSTICA 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. 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. 2017-04-11T20:33:35Z 2017-04-11T20:33:35Z 2017-02-15 masterThesis XAVIER, Bruno Francisco. Formalização da lógica linear em Coq. 2017. 63f. Dissertação (Mestrado em Matemática Aplicada e Estatística) - Centro de Ciências Exatas e da Terra, Universidade Federal do Rio Grande do Norte, Natal, 2017. https://repositorio.ufrn.br/jspui/handle/123456789/22622 por Acesso Aberto application/pdf Brasil UFRN PROGRAMA DE PÓS-GRADUAÇÃO EM MATEMÁTICA APLICADA E ESTATÍSTICA |