Tese (doutorado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2017. / Texto parcialmente liberado pelo autor. Conteúdo restrito: Capítulos 1 e 2. / Submitted by Raquel Almeida (raquel.df13@gmail.com) on 2017-11-07T20:17:47Z No. of bitstreams: 1 2017_PedroManuelSánchezAguilar_PARCIAL.pdf: 384580 bytes, checksum: 0a2caa6edca02281ed6594a4c17ea88b (MD5) / Approved for entry into archive by Patrícia Nunes da Silva (patricia@bce.unb.br) on 2018-06-04T13:51:46Z (GMT) No. of bitstreams: 1 2017_PedroManuelSánchezAguilar_PARCIAL.pdf: 384580 bytes, checksum: 0a2caa6edca02281ed6594a4c17ea88b (MD5) / Made available in DSpace on 2018-06-04T13:51:46Z (GMT). No. of bitstreams: 1 2017_PedroManuelSánchezAguilar_PARCIAL.pdf: 384580 bytes, checksum: 0a2caa6edca02281ed6594a4c17ea88b (MD5) Previous issue date: 2018-06-04 / CNPq / O objetivo deste trabalho é estudar a existência, multiplicidade e não existência de soluções para problemas elípticos não-lineares dependendo de um parâmetro sob uma hipótese do tipo Landesman-Lazer. Para estabelecer a existência de solução combinamos o Método de Redução de Lyapunov-Schmidt e a técnica de congelamento do termo gradiente com argumentos de truncamento e aproximação através de métodos de bootstrap. Não há restrição de crescimento no infinito sobre o termo não-linear o qual pode mudar de sinal. / The purpose of this work is to study existence, multiplicity and non existence of solutions for nonlinear elliptic problems depending on a parameter under Landesman-Lazer type hypotheses. In ordem to establish the existence of solution we combine the Lyapunov-Schmidt Reduction Method and the term gradient freeze technique with truncation and approximation arguments via bootstrap methods. There is no growth restriction at infinity on the nonlinear term and it may change sign.

Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2007. / Submitted by Kathryn Cardim Araujo (kathryn.cardim@gmail.com) on 2009-12-15T16:01:29Z No. of bitstreams: 1 dissert_Maryane da Silva Moreira F.pdf: 345089 bytes, checksum: 1de0d038d6f193b27ba4b96d0f0af765 (MD5) / Approved for entry into archive by Lucila Saraiva(lucilasaraiva1@gmail.com) on 2009-12-15T21:19:16Z (GMT) No. of bitstreams: 1 dissert_Maryane da Silva Moreira F.pdf: 345089 bytes, checksum: 1de0d038d6f193b27ba4b96d0f0af765 (MD5) / Made available in DSpace on 2009-12-15T21:19:16Z (GMT). No. of bitstreams: 1 dissert_Maryane da Silva Moreira F.pdf: 345089 bytes, checksum: 1de0d038d6f193b27ba4b96d0f0af765 (MD5) Previous issue date: 2007-08-24 / Problemas de Riemann modelam escoamentos de fluidos trifásicos em meios porosos. Estudamos as noções de alguns tipos de problemas de Riemann e de suas soluções, utilizando o critério de entropia de viscosidade. Obtemos uma forma normal para o sistema 2 x 2 de leis de conservação [14] e examinamos o papel dos choques transicionais nas soluções de problemas de Riemann, verificando em que circunstâncias estes choques possuem perfil reto [9]. Por fim, verificamos que o conjunto de soluções está associado a uma variedade que se assemelha a um para um helicóide [1]. Em seguida, modificamos uma das entradas da matriz de viscosidade identidade e comprovamos que o helicóide de soluções ainda existe. A maior parte desta dissertação está baseada em [1], [9] e [14]. ____________________________________________________________________________________________ ABSTRACT / Riemann Problems model three phase flow in porous media. We study the basic notions of some type of Riemann problems and their solutions, using the viscous profile criterium. We obtain a normal form to the 2 × 2 system of conservation laws [14] and we examine the role of the transicional shocks in Riemann solutions checking in which circunstances these shocks posses straight line profiles [9]. Finally, we verify that the set of solutions is associated to a manifold that looks like an helicoid, for an example in which the viscosity matrix is the identity [1]. Next, we modify one of the zero entries of the identity viscosity matrix and we confirm that the helicoid of solutions still exists. The main part of this dissertation is based on [1], [9] and [14].

Dissertação (Mestrado em Matemática)-Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, Brasília, 2010. / Submitted by Jaqueline Ferreira de Souza (jaquefs.braz@gmail.com) on 2011-06-29T20:35:37Z No. of bitstreams: 1 2010_EduardoAntoniodaSilva.pdf: 399866 bytes, checksum: 5f8d410b8277fdf6678fff120e8d8b18 (MD5) / Approved for entry into archive by Jaqueline Ferreira de Souza(jaquefs.braz@gmail.com) on 2011-06-29T20:36:12Z (GMT) No. of bitstreams: 1 2010_EduardoAntoniodaSilva.pdf: 399866 bytes, checksum: 5f8d410b8277fdf6678fff120e8d8b18 (MD5) / Made available in DSpace on 2011-06-29T20:36:12Z (GMT). No. of bitstreams: 1 2010_EduardoAntoniodaSilva.pdf: 399866 bytes, checksum: 5f8d410b8277fdf6678fff120e8d8b18 (MD5) / Seja f um difeomorfismo de classe Cr, r ≥ 2 de uma superficie M², e seja ∆ uma ferradura de f (isto é, um conjunto hiperbólico transitivo e isolado). É um resultado clássico que existe uma vizinhança U de ∆ tal que para todo difeomorfismo próximo de f na topologia Cr o conjunto ∆g = ∩ gn (∪) é uma ferradura de g. Nós provaremos um resultado de Mañé [3] que fornece uma vizinhança U de f na topologia Cr tal que a aplicação U ∃ g → HD(∆ g) ϵR R é uma função Cr de g. ______________________________________________________________________________________ ABSTRACT / Let f be a Cr diffeomorphism r ≥ 2 of a surface M2, and let ∆ a horseshoe of f (i.e, a transitive and isolated hiperbolic set). It is a classical result that exists a neighborhood U of such that for every diffeomorphism close to f in Cr topology the set ∆ g = ∩ gn (∪) is a horseshoe for g. We will prove a result of Mañé [3] that provides there exist a Cr neighborhood U of f such that, the map U ∃ g → HD(∆ g) ϵR is a Cr function of g.

Orientadores: Marko Antonio Rojas Medar, Mario Duran Toro / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Matematica Estatistica e Computação Cientifica / Made available in DSpace on 2018-08-08T17:45:04Z (GMT). No. of bitstreams: 1 Cabrales_RobertoCarlos_D.pdf: 5170211 bytes, checksum: db848279a41dc57e3812aca09a5b3966 (MD5) Previous issue date: 2007 / Resumo: O estudo dos processos de solidificação de metais e ligas é um dos problemas mais complexos da engenharia, tanto do ponto de vista teórico como tecnológico A complexa natureza dos fenômenos físicos envolvidos fazem impossível a obtenção de soluções de forma simples. Por isto, temos que usar sofisticados modelos matemáticos formados por sistemas de equações diferenciais em derivadas parciais de evolução e não lineares. No presente trabalho estamos preocupados dos aspectos computacionais da solidificação de ligas binárias: apresentamos um algoritmo numérico que está baseado no método dos volumes finitos em malhas colocalizadas e o método de Euler implícito para o avanço no tempo. Diversos problemas documentados na literatura são usados para verificar a implementação dos algoritmos. Também, apresentamos simulações numéricas que caracterizam e verificam numericamente a formação de canais de convecção / Abstract: The study of metals solidification processes and alloys is a very complex problem in engineering, from the theoretical point of view and from the technological point of view. By the complex nature of the physical phenomena involved it is impossible to find solutions of simple nature. So, we have to use sophisticated mathematical models consisting of non-linear time dependent partial differential equations. In this work we are concerned with the computational aspect of the solidification of binary alloys: we present a numerical algorithm based in the finite volume method in co-located grids and the implicit Euler method for time advancing. Several problems documented in the literature are used to verify the implementation of the algorithms. Second, we present numerical simulations characterizing and validating the freckles formation / Doutorado / Doutor em Matemática Aplicada

Orientador: João Frederico C. A. Meyer / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Matematica, Estatistica e Computação Científica / Made available in DSpace on 2018-07-14T02:38:18Z (GMT). No. of bitstreams: 1 Mistro_DiomarCristina_M.pdf: 2371505 bytes, checksum: 050338393f92949fd8aba29304c1bfac (MD5) Previous issue date: 1992 / Resumo: Não informado. / Abstract: Not informed. / Mestrado / Mestre em Matemática Aplicada

Orientador: Antonio Jose Engler / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Matematica, Estatistica e Computação Científica / Made available in DSpace on 2018-07-17T01:29:37Z (GMT). No. of bitstreams: 1 Cavichia_MarioConrado_M.pdf: 1759348 bytes, checksum: d8f00d75ce4df1053ab4bbe195373e5e (MD5) Previous issue date: 1988 / Resumo: Não informado. / Abstract: Not informed. / Mestrado / Mestre em Matemática

A equação de complexidade de um algoritmo pode ser expressa em termos de uma equação de recorrência. A partir destas equações obtém-se uma expressão assintótica para a complexidade, provada por indução. Neste trabalho, propõem-se um esquema de solução de equações de recorrência usando equações características que são resolvidas através de um "software" de computação simbólica, resultando em uma expressão algébrica exata para a complexidade. O objetivo é obter uma forma geral de calcular a complexidade de um algoritmo desenvolvido pelo método Divisão-e-Conquista.

Tese(doutorado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2008. / Submitted by Ruthléa Nascimento (ruthlea@bce.unb.br) on 2008-10-30T16:12:50Z No. of bitstreams: 1 2008_AndreLuizGaldino.pdf: 873327 bytes, checksum: ea02527f0563d16fc5b1df77c3f6f722 (MD5) / Approved for entry into archive by Luanna Maia(luanna@bce.unb.br) on 2009-02-26T15:02:00Z (GMT) No. of bitstreams: 1 2008_AndreLuizGaldino.pdf: 873327 bytes, checksum: ea02527f0563d16fc5b1df77c3f6f722 (MD5) / Made available in DSpace on 2009-02-26T15:02:00Z (GMT). No. of bitstreams: 1 2008_AndreLuizGaldino.pdf: 873327 bytes, checksum: ea02527f0563d16fc5b1df77c3f6f722 (MD5) / Teorias para Sistemas Abstratos de Redução (ARS) e Sistemas de Reescrita de Termos (TRS) no assistente de provas PVS (Prototype Verification System) chamadas ars e trs, respectivamente, foram desenvolvidas. A teoria ars, construída com base na teoria para relações binárias do PVS, contém especificações de noções tais como redução, confluência, formas normais, e conceitos não básicos como por exemplo noeterianidade. Por outro lado, a teoria trs, construída com base na teoria ars e a teoria para seqüências finitas encontrada na biblioteca do PVS, contém uma formalização para lidar com a estrutura dos termos, assim como, formalizações de noções não triviais de TRS. As teorias ars e trs foram desenvolvidas com o objetivo de agregar os conceitos e as definições necessários para lidar com a Teoria de Reescrita, em geral. Em outras palavras, ars e trs contém elementos que formam uma base sólida para formalizar propriedades da Teoria de Reescrita em PVS. Para certificar-se de que o objetivo foi alcançado vários resultados bem conhecidos e não triviais foram formalizados; dentre estes, destacam-se a correção do princípio de indução Noeteriana, o Lema de Newman, os Lemas de Comutação e o Teorema dos Pares Críticos de Knuth-Bendix. Além de constituir uma base para formalização de propriedades da Teoria de Reescrita, em geral, a formalização apresentada se destaca por: 1. utilizar uma linguagem de orderm superior, a qual permite expressar naturalmente propriedades de ordem superior; 2. por seu alto grau de abstração, que permite expressar propriedades numa forma quasi-geométrica, como desejável em Teoria de Reescrita; e, 3. pelo alto grau de controle, permitido pelo PVS, no desenvolvimento das provas. _______________________________________________________________________________________ ABSTRACT / Theories for Abstract Reduction Systems (ARS) and Term Rewriting Systems (TRS) in the proof assistant PVS (Prototype Verification System) called ars and trs, respectively, we developed. The ars theory built on the PVS library for binary relations, contains specifications of notions such as reduction, confluence, normal forms, and non basic concepts such as Noetherianity. On the other hand, the trs theory built on the ars theory and the PVS library for finite sequences, contains a formalization to deal with the structure of terms as well as formalizations of non-trivial notions of TRS. Theories ars and trs were developed with the main goal of providing the necessary concepts and definitions to deal with the Theory of Rewriting in general. In other words, ars and trs contain elements that conform a solid basis to formalize properties of the Theory of Rewriting in PVS. To make sure that the goal was achieved well-known and non-trivial results were formalised; among these, the correctness of the principle of noetherian induction, the Newman’s Lemma, the Commutation Lemma and the Knuth-Bendix Critical Pair Theorem. Apart from being a basis for formalization of properties of the Theory of Rewriting, in general, the formalization presented is highlighted by: 1. the use a higherorder language, which allows for the specification of high-order properties naturally, 2. for their high-level of abstraction, which allows for the specification properties in an almost geometric style, as desirable in Rewriting Theory, and 3. the high degree of control allowed by PVS in the development of proofs.

A equação de complexidade de um algoritmo pode ser expressa em termos de uma equação de recorrência. A partir destas equações obtém-se uma expressão assintótica para a complexidade, provada por indução. Neste trabalho, propõem-se um esquema de solução de equações de recorrência usando equações características que são resolvidas através de um "software" de computação simbólica, resultando em uma expressão algébrica exata para a complexidade. O objetivo é obter uma forma geral de calcular a complexidade de um algoritmo desenvolvido pelo método Divisão-e-Conquista.

A equação de complexidade de um algoritmo pode ser expressa em termos de uma equação de recorrência. A partir destas equações obtém-se uma expressão assintótica para a complexidade, provada por indução. Neste trabalho, propõem-se um esquema de solução de equações de recorrência usando equações características que são resolvidas através de um "software" de computação simbólica, resultando em uma expressão algébrica exata para a complexidade. O objetivo é obter uma forma geral de calcular a complexidade de um algoritmo desenvolvido pelo método Divisão-e-Conquista.