Submitted by Sandra Pereira (srpereira@ufrrj.br) on 2017-04-24T14:13:26Z No. of bitstreams: 1 2012 - Ana Carolina Bello de Souza.pdf: 1911170 bytes, checksum: 62c70571aeb2100b8313dc1ef44eac2b (MD5) / Made available in DSpace on 2017-04-24T14:13:26Z (GMT). No. of bitstreams: 1 2012 - Ana Carolina Bello de Souza.pdf: 1911170 bytes, checksum: 62c70571aeb2100b8313dc1ef44eac2b (MD5) Previous issue date: 2012-10-03 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior - CAPES / In this work, the theoretical study of the gas-phase bimolecular nucleophilic substitution reaction, CH3Cl + OH- CH3OH + Cl-, is introduced, aiming the description of the potential energy surface, the calculation of rate constants and the investigation of the effect of increasing the side chain (changing the CH3 radical in the reaction cited above by the radicals ethyl, n-propyl, i-propyl, n-butyl, s-butyl e t-butyl). The theoretical calculations have been first performed at the MP2/6-31+G(d) level for the geometry optimizations and vibrational frequencies calculations. Single point calculations at the CCSD(T)/6-31+G(d) level have also been performed in order to improve the total energies for the stationary points. However, the relative energies of these stationary points at both MP2 and CCSD(T) level shown close results, so that the single point calculations at the CCSD(T) level have not been proved strictly necessary and have therefore not been performed for all the points along the potential energy surface. The minimum energy path has been described by the intrinsic reaction coordinate method, calculated at the MP2/6-31+G(d) by performing sequential geometry optimizations starting from the saddle point. The calculated enthalpy difference at 298K for the reaction has been determined as -49.5 kcal/mol, in good agreement with the literature value: -50.5 kcal/mol. The calculated rate constant has been obtained as 1.41 x 10-9 cm3.molecule-1.s-1, at 298,15K, in excellent agreement with the experimental data: 1.3 ? 1.6 x 10-9 cm3.molecule-1.s-1.Moreover, the rate constants show non-Arrhenius behavior, decreasing as the temperature increases, which is consistent with the experimental expectation. In this way, the performance of the variational transition state theory for this reaction can be considered satisfactory. By increasing the side chain of the reactant, other reaction channels have been observed: the bimolecular elimination E2 channel and the attack of the nucleophile from the same plane of the exit group (the front-SN2).For these reactions of the alkyl chlorides on n carbon atoms (1 < n ? 4), the B3LYP/6-31+G(d,p) level has been adopted for geometry optimizations and vibrational frequencies. Then, single point calculations at the CCSD(T)/6-31+G(d,p)//B3LYP/6- 31+G(d,p) level have been performed. A comparison of the reaction channels, back- SN2 and E2, shows that the E2 channel is kinetically favored, whereas the SN2 products are thermodynamically more stable. As expected, high values for the potential height have been observed for the front-SN2, being these channels disfavored in all cases. In general, the energy of the saddle points in respect to the isolated reactants slightly depend upon the size of the side chain. / Este trabalho trata do estudo te?rico das rea??es de substitui??o nucleof?lica de segunda ordem, CH3Cl + OH- CH3OH + Cl-, em fase gasosa, visando estudar a superf?cie de energia potencial, obter as constantes de velocidade e ainda verificando o efeito do aumento da cadeia lateral (trocando o radical CH3 na rea??o descrita acima por radicais etil, n-propil, i-propil, n-butil, s-butil e t-butil). Primeiramente, c?lculos te?ricos para otimiza??es de geometria e frequ?ncia foram realizados em n?vel MP2/6-31+G(d) para a rea??o CH3Cl + OH- CH3OH + Cl- e, em seguida, c?lculos single-point em n?vel CCSD(T)/6-31+G(d) foram realizados para corrigir os valores da energia eletr?nica dos pontos estacion?rios obtidos no caminho de rea??o. Entretanto, os valores obtidos para as energias relativas em n?veis MP2 e CCSD(T) foram muito pr?ximos, n?o sendo estritamente necess?rio refinar,atrav?s de c?lculos single-point em n?vel CCSD(T)/6- 31+G(d),os valores de energia de todos os pontos obtidos na superf?cie de energia potencial. O caminho de rea??o menor energia foi descrito pela coordenada de rea??o intr?nseca, calculada por otimiza??es de geometrias de uma sequ?ncia de configura??es ao redor do ponto de sela em n?vel MP2/6-31+G(d). A diferen?a de entalpia a 298K calculada para a rea??o foi de -49,5 kcal/mol, em bom acordo com o dado da literatura, -50,5 kcal/mol. A constante de velocidade da rea??o obtida foi de 1,41 x 10-9 cm3.mol?cula-1.s-1, a 298,15K, em excelente acordo com o dado experimental: 1,3 ? 1,6 x 10-9 cm3.mol?cula-1.s-1. Al?m disso, as constantes de velocidade globais apresentam comportamento n?o-Arrhenius, diminuindo conforme a temperatura aumenta, em um perfil consistente com a observa??o experimental. Dessa forma, a aplica??o da teoria de estado de transi??o se mostra satisfat?ria para essa rea??o. A partir do aumento da cadeia lateral, outros canais de rea??o foram observados, em prov?vel competi??o ? substitui??o nucleof?lica de ordem 2: a elimina??o de segunda ordem, E2. O ataque do nucle?filo pela frente da cadeia tamb?m foi obtido e investigado. Para as rea??es dos cloretos de alquila com cadeia lateral de n carbonos (1 < n ? 4), o n?vel B3LYP/6- 31+G(d,p) foi adotado para c?lculos de otimiza??es e frequ?ncias. Posteriormente, c?lculos em n?vel CCSD(T)/6-31+G(d,p)//B3LYP/6-31+G(d,p) foram realizados. Comparando os canais de rea??o de substitui??o nucleof?lica back e de elimina??o, o canal cineticamente favorecido foi o de elimina??o, por?m os produtos termodinamicamente mais est?veis s?o os de substitui??o nucleof?lica. Como esperado, observa-se uma barreira de potencial muito alta para as rea??es substitui??o pela frente, sendo esses canais desfavorecidos em todos os casos.Em geral, a diferen?a de energia dos pontos de sela em rela??o aos reagentes isolados mostra pequena depend?ncia com o aumento da cadeia lateral linear

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.

Made available in DSpace on 2014-12-17T15:28:51Z (GMT). No. of bitstreams: 1 BrunaSL_DISSERT.pdf: 1891001 bytes, checksum: 1d482b920c53ec1f846060dbc2158ebb (MD5) Previous issue date: 2012-08-10 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / The cerebral cortex of mammals is histologically organized into different layers of excitatory neurons that have distinct patterns of connections with cortical or subcortical targets. During development, these cortical layers are established through an intricate combination of neuronal specification and migration in a radial pattern known as "insideout": deep-layer neurons are generated prior to upper-layer neurons. In the last few decades, several genes encoding transcription factors involved in the sequential specification of neurons destined to different cortical layers have been identified. However, the influence of early-generated neurons in the specification of subsequent neuronal cohorts remains unclear. To investigate this possible influence, we induced the selective death of cortical neurons from layer V and VI before the generation of layer II, III and IV neurons. Thus, we can evaluate the effects of ablation of early born neurons on the phenotype of late born neurons. Our data shows that one-day after ablation, layer VI neurons expressing the transcription factor TBR1 are newly generated while virtually no neuron expressing TBR1 was generated in the same age in control animals. This suggests that progenitors involved in the generation of neurons destined for superficial layers suffer interference from the selective death of neurons in deep layers, changing their specification. We also observed that while TBR1-positive neurons are located exclusively in deep cortical layers of control animals, many TBR1-positive neurons are misplaced in superficial layers of ablated animals, suggesting that the migration of cortical neurons could be controlled independently of neuronal phenotypes. Furthermore, we observed an increase in layer V neurons expressing CTIP2 and neurons expressing SATB2 and that these cells have changed their distributions. As a conclusion, our data indicate the existence of a mechanism of control exercised by the early-generated neurons in the cerebral cortex on the fate of the progenitors involved in the generation of the following cortical neurons. This mechanism could help to control the number of neurons in different layers and contribute to the establishment of different cortical areas / O c?rtex cerebral de mam?feros encontra-se histologicamente organizado em camadas de neur?nios excitat?rios que, por sua vez, apresentam distintos padr?es de conectividade com alvos corticais ou sub-corticais. Durante o desenvolvimento, estas camadas corticais s?o estabelecidas atrav?s de uma intrincada combina??o entre especifica??o neuronal e migra??o radial num padr?o conhecido como "inside-out" (de dentro para fora). Desta forma, por exemplo, neur?nios infragranulares nas camadas V e VI s?o gerados anteriormente aos neur?nios granulares da camada IV, que por sua vez s?o gerados antes dos supra-granulares das camadas II e III. Na ?ltima d?cada, foram identificados diversos genes codificando fatores de transcri??o envolvidos na especifica??o sequencial de neur?nios destinados ?s diferentes camadas corticais. No entanto, ainda pouco ? sabido sobre a influ?ncia dos neur?nios gerados previamente sobre a especifica??o das coortes neuronais subsequentes. Para investigar esta poss?vel influ?ncia, n?s utilizamos um m?todo de recombina??o g?nica (sistema Cre- Lox) para induzir a morte seletiva de neur?nios das camadas corticais V e VI antes da gera??o dos neur?nios das camadas II, III e IV. Dessa forma, pudemos avaliar os efeitos da abla??o de neur?nios infragranulares sobre o fen?tipo dos neur?nios gerados em seguida. Nossos dados mostraram que, um dia ap?s a abla??o, neur?nios da camada VI expressando o fator de transcri??o TBR1 voltaram a ser gerados enquanto praticamente nenhum neur?nio expressando TBR1 foi gerado na mesma idade em animais controle. Esse dado sugere que os progenitores envolvidos na gera??o de neur?nios destinados ?s camadas superficiais sofrem interfer?ncia da morte seletiva de neur?nios de camadas profundas, mudando sua especifica??o. Uma parte dos neur?nios TBR1 se estabeleceu na camada VI e outra migrou at? as camadas II e III, indicando que o controle dos padr?es migrat?rios pode ser independente dos fen?tipos neuronais. Al?m disso, observamos que na popula??o neuronal total tamb?m ocorreu um aumento na quantidade de neur?nios de camada V expressando CTIP2 e uma altera??o na distribui??o dessas c?lulas. O mesmo foi observado para neur?nios supragranulares expressando SATB2. Em conjunto, nossos dados indicam a exist?ncia de um mecanismo de controle exercido pelos neur?nios gerados inicialmente no c?rtex cerebral sobre o destino dos progenitores envolvidos na gera??o dos demais neur?nios corticais. Tal mecanismo poderia contribuir para o controle do n?mero de neur?nios em diferentes camadas e contribuir para o estabelecimento de diferentes ?reas corticais

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.