Spelling suggestions: "subject:"L?gico linear""
1 |
Um estudo de l?gica linear com subexponenciais / A study of linear logic with subexponentialsOrto, Laura Fernandes Dell 15 February 2017 (has links)
Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2017-04-03T22:46:24Z
No. of bitstreams: 1
LauraFernandesDellOrto_DISSERT.pdf: 866111 bytes, checksum: 0ef11e74d1508214463b993885352d6c (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2017-04-11T20:56:41Z (GMT) No. of bitstreams: 1
LauraFernandesDellOrto_DISSERT.pdf: 866111 bytes, checksum: 0ef11e74d1508214463b993885352d6c (MD5) / Made available in DSpace on 2017-04-11T20:56:41Z (GMT). No. of bitstreams: 1
LauraFernandesDellOrto_DISSERT.pdf: 866111 bytes, checksum: 0ef11e74d1508214463b993885352d6c (MD5)
Previous issue date: 2017-02-15 / Em L?gica Cl?ssica, podemos utilizar as hip?teses um n?mero indeterminado de vezes.
Por exemplo, a prova de um teorema pode fazer uso do mesmo lema v?rias vezes. Por?m,
em sistemas f?sicos, qu?micos e computacionais a situa??o ? diferente: um recurso n?o
pode ser reutilizado ap?s ser consumido em uma a??o. Em L?gica Linear, f?rmulas s?o
vistas como recursos a serem utilizados durante a prova. ? essa no??o de recursos que
faz a L?gica Linear ser interessante para a modelagem de sistemas. Para tanto, a L?gica
Linear controla o uso da contra??o e do enfraquecimento atrav?s dos exponenciais ! e
?. Este trabalho tem como objetivo fazer um estudo sobre a L?gica Linear com Subexponenciais
(SELL), que ? um refinamento da L?gica Linear. Em SELL, os exponenciais
da L?gica Linear possuem ?ndices, isto ?, ! e ? ser?o substitu?dos por !i e ?i, onde ?i? ?
um ?ndice. Um dos pontos fundamentais de Teoria da Prova ? a prova da Elimina??o do
Corte, que neste trabalho ? demonstrada tanto para L?gica Linear como para SELL, onde
apresentamos detalhes que normalmente s?o omitidos. A partir do teorema de Elimina??o
do Corte, podemos concluir a consist?ncia do sistema (para as l?gicas que estamos
utilizando) e outros resultados como a propriedade de subf?rmula. O trabalho inicia-se
com um cap?tulo de Teoria da Prova, e em seguida se faz uma exposi??o sobre a L?gica
Linear. Assim, com essas bases, apresenta-se a L?gica Linear com Subexponenciais. SELL
tem sido utilizada, por exemplo, na especifica??o e verifica??o de diferentes sistemas tais
como sistemas bioqu?micos, sistemas de intera??o multim?dia e, em geral, em sistemas
concorrentes com modalidades temporais, espaciais e epist?micas. Com essa base te?rica
bastante clara, apresenta-se a especifica??o de um sistema bioqu?mico utilizando SELL.
Al?m disso, apresentamos v?rias inst?ncias de SELL que tem interpreta??es interessantes
do ponto de vista computacional. / In Classical Logic, we can use a given hypothesis an indefinite number of times. For
example, the proof of a theorem may use the same lemma several times. However, in
physical, chemical and computational systems, the situation is different: a resource cannot
be reused after being consumed in one action. In Linear Logic, formulas are seen
as resources to be used during a proof. This feature makes Linear Logic an interesting
formalism for the specification and verification of such systems. Linear Logic controls the
rules of contraction and weakening through the exponentials ! and ?. This work aims to
study Linear Logic with subexponentials (SELL), which is a refinement of Linear Logic.
In SELL, the exponentials of Linear Logic are decorated with indexes, i.e., ! and ? are
replaced with !i and ?i, where ?i? is an index. One of the main results in Proof Theory is
the Cut-Elimination theorem. In this work we demonstrate that theorem for both Linear
Logic and SELL, where we present details that are usually omitted in the literature. From
the Cut-Elimination Theorem, we can show, as a corollary, the consistency of the system
(for the logics considered here) and other results as the subformula property. This work
begins with an introduction to Proof Theory and then, it presents Linear Logic. On these
bases, we present Linear Logic with subexponentials. SELL has been used, for example,
in the specification and verification of various systems such as biochemical systems, multimedia
interaction systems and, in general, concurrent systems with temporal, spatial
and epistemic modalities. Using the theory of SELL, we show the specification of a biochemical
system. Moreover, we present several instances of SELL that have interesting
interpretations from a computational point of view.
|
2 |
Formaliza??o da l?gica linear em CoqXavier, Bruno Francisco 15 February 2017 (has links)
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.
|
Page generated in 0.0475 seconds