Submitted by Luciana Ferreira (lucgeral@gmail.com) on 2016-09-09T12:27:04Z No. of bitstreams: 2 Tese - Tharsis Souza Silva - 2016.pdf: 3242823 bytes, checksum: 4cdf7de6c7ba7cfe6f4fc07cc9501592 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Approved for entry into archive by Luciana Ferreira (lucgeral@gmail.com) on 2016-09-09T12:27:26Z (GMT) No. of bitstreams: 2 Tese - Tharsis Souza Silva - 2016.pdf: 3242823 bytes, checksum: 4cdf7de6c7ba7cfe6f4fc07cc9501592 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2016-09-09T12:27:26Z (GMT). No. of bitstreams: 2 Tese - Tharsis Souza Silva - 2016.pdf: 3242823 bytes, checksum: 4cdf7de6c7ba7cfe6f4fc07cc9501592 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2016-05-13 / Fundação de Amparo à Pesquisa do Estado de Goiás - FAPEG / In this work we _rstly study a relay system X on the Rn that, under certain conditions, it has a one parameter family of 1-periodic orbits that arises in the origin and increase inde_nitely. We study yet another relay system class X_, that it is formed from the initial relay system by aditions of nilpotent parameters that, under certain conditions, it has the same result of the previous, and yet family of periodic orbits that arises in the origin and ends in a loop, or family that bifurcate of a loop and arise inde_nitelly. Furthermore the periodic solutions are explicitely given by Euler polynomials. Finally we study a third order di_erential equation with relay looking for periodic orbits of di_erent degrre of di_erentiability and this is done by the associated vector _eld with jump. / Neste trabalho estudamos primeiramente um campo vetorial descontínuo com chaveamento X atuando no Rn que, sob certas condições, possui uma família a um parâmetro de órbitas 1-periódicas que surge na origem e cresce indenidamente. Estudamos também uma classe de campos vetoriais descontínuos com chaveamento (relay systems) X, que se diferencía do campo inicial pela adição de parâmetros i;j de forma linear Nilpotente que, sob certas condições, possui o mesmo resultado que o caso anterior, e ainda famílias que surgem na origem e termina em um Laço ou mesmo que bifurcam de um laço e crescem indenidamente. Além disso as soluções periódicas são dadas explicitamente através dos polinômios de Euler. Ainda estudamos uma equação diferencial de terceira ordem com chaveamento a m de buscar órbitas periódicas de diferentes graus de diferenciabilidade e esse estudo é feito através do campo vetorial associado com impulso.

Semantic Image Interpretation (SII) is the process of generating a structured description of the content of an input image. This description is encoded as a labelled direct graph where nodes correspond to objects in the image and edges to semantic relations between objects. Such a detailed structure allows a more accurate searching and retrieval of images. In this thesis, we propose two well-founded methods for SII. Both methods exploit background knowledge, in the form of logical constraints of a knowledge base, about the domain of the images. The first method formalizes the SII as the extraction of a partial model of a knowledge base. Partial models are built with a clustering and reasoning algorithm that considers both low-level and semantic features of images. The second method uses the framework Logic Tensor Networks to build the labelled direct graph of an image. This framework is able to learn from data in presence of the logical constraints of the knowledge base. Therefore, the graph construction is performed by predicting the labels of the nodes and the relations according to the logical constraints and the features of the objects in the image. These methods improve the state-of-the-art by introducing two well-founded methodologies that integrate low-level and semantic features of images with logical knowledge. Indeed, other methods, do not deal with low-level features or use only statistical knowledge coming from training sets or corpora. Moreover, the second method overcomes the performance of the state-of-the-art on the standard task of visual relationship detection.

Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some theory or combination of theories; Verification Modulo Theories (VMT) is the problem of analyzing the reachability for transition systems represented in terms of SMT formulae. In this thesis, we tackle the problems of SMT and VMT over the theories of polynomials over the reals (NRA), over the integers (NIA), and of NRA augmented with transcendental functions (NTA). We propose a new abstraction-refinement approach called Incremental Linearization. The idea is to abstract nonlinear multiplication and transcendental functions as uninterpreted functions in an abstract domain limited to linear arithmetic with uninterpreted functions. The uninterpreted functions are incrementally axiomatized by means of upper- and lower-bounding piecewise-linear constraints. In the case of transcendental functions, particular care is required to ensure the soundness of the abstraction. The method has been implemented in the MathSAT SMT solver, and in the nuXmv VMT model checker. An extensive experimental evaluation on a wide set of benchmarks from verification and mathematics demonstrates the generality and the effectiveness of our approach. Moreover, the proposed technique is an enabler for the (nonlinear) VMT problems arising in practical scenarios with design environments such as Simulink. This capability has been achieved by integrating nuXmv with Simulink using a compilation-based approach and is evaluated on an industrial-level case study.

Made available in DSpace on 2015-03-04T18:50:39Z (GMT). No. of bitstreams: 1 thesis.pdf: 4735629 bytes, checksum: efd1eaf8c6c6b15b99b84eb0d25bd102 (MD5) Previous issue date: 2012-09-06 / Coordenacao de Aperfeicoamento de Pessoal de Nivel Superior / Multiphase flows in porous media are modeled by a system of partial differential equations and the study of the numerical approximation to the solutions of these plays a crucial role in the simulation and prediction of problems that are of great practical interest and of economic and social impact, such as secondary oil recovery, geological storage of CO2 and transport of pollutants in aquifers. The goal of this work is the development of a three-dimensional numerical simulator that precisely evaluates the transport of two immiscible fluids in a heterogeneous porous media using multithread parallel programming to shared memory multiprocessors computers. The system of partial differential equations is decomposed into a elliptic subsystem used to determine the velocity field and into a hyperbolic equation (nonlinear) to determine the transport of the fluid phases. The approximation to the solution of the latter one is calculated using a high order non-oscillatory finite-differences numerical method based on central schemes that allows a semi-discrete formulation which an extension that enables to work with variable space coefficients. Numerical experiments on three-dimensional models were performed considering linear and nonlinear flow problems in typical settings of oil reservoirs simulations. The results were satisfactory since they presented mass conservation, precise capture of shock waves and small numeric diffusion, regardless of the time step. / Escoamentos multifásicos em meios porosos são modelados por um sistema de equações diferenciais parciais e o estudo da aproximação das soluções dessas equações desempenha papel crucial na simulação e previsão de problemas de grande interesse prático e impacto econômico e social, tais como a recuperação secundária de petróleo, o armazenamento geológico de CO2 e o transporte de poluentes em aquíferos. O presente trabalho tem como objetivo o desenvolvimento de um simulador numérico tridimensional para avaliar com precisão o transporte de dois fluidos imiscíveis em um meio poroso heterogêneo e que utiliza computação paralela multithread para computadores multiprocessados de memória compartilhada. O sistema de equações diferenciais parciais é decomposto em um subsistema elíptico para a determinação do campo de velocidades dos fluidos e uma equação hiperbólica não-linear para o transporte das fases fluidas. Para esta última, foi utilizado um método numérico de volumes finitos, não-oscilatório de alta ordem baseado em esquemas centrais e que admite uma formulação semi-discreta com coeficientes variáveis no espaço. Experimentos numéricos em modelos tridimensionais foram realizados considerando problemas de escoamentos lineares e não lineares postos em configurações típicas de simulação de reservatórios de petróleo. Os resultados mostraram-se satisfatórios por apresentarem conservação da massa, boa captura das ondas de choque e pequena difusão numérica, independente do passo de tempo.

Conselho Nacional de Desenvolvimento CientÃfico e TecnolÃgico / O termo Teoria da Prova foi introduzido por Hilbert para identificar o estudo sobre provas formais. Pesquisas nessa Ãrea podem ser classificadas em: a) Teoria da Prova Redutiva ou Interpretacional, cujo objetivo à demonstrar, entre outras coisas, a consistÃncia da matemÃtica utilizando somente mÃtodos finitistas, e b) Teoria da Prova Estrutural, onde caracterÃsticas estruturais das provas formais sÃo investigadas por meio de sistemas dedutivos como DeduÃÃo Natural e CÃlculo de Sequentes. Prawitz, por meio da Teoria da Prova, definiu uma Teoria dos Significados para constantes logicas e propÃs regras esquemÃticas de introduÃÃo e de eliminaÃÃo para caracterizar os conectivos proposicionais. Schroeder-Heister estendeu as definiÃÃes de Prawitz e formalizou o uso de regras como hipÃteses, tornando possÃvel a utilizaÃÃo de cÃlculos para suposiÃÃes separados de cÃlculos para constantes lÃgicas. NÃo estamos interessados na investigaÃÃo de regras esquemÃticas para dar significado a constantes lÃgicas. Pretendemos, na verdade, definir procedimentos de normalizaÃÃo esquemÃticos, baseados em tais regras esquematicas, com objetivo de identificar condiÃÃes suficientes para um sistema ser normalizÃvel. Tais resultados sÃo pertinentes à Teoria Abstrata da Prova, termo usado para identificar o estudo das condiÃÃes abstratas e gerais para a anÃlise prova-teÃrica de sistemas formais. Teoria Abstrata da Prova nÃo estuda cÃlculos lÃgicos especÃficos, mas famÃlias de cÃlculos instÃncias de regras esquemÃticas. A nossa proposta, portanto, baseia-se em regras esquemÃticas que podem ser instanciadas por regras concretas, em particular, por regras que introduzem operadores modais. Provamos, tambÃm, Teoremas de NormalizaÃÃoo Fraca e Forte para sistemas esquemÃticos definidos em funÃÃoo de nossas regras esquemÃticas, obtemos condiÃÃes suficientes para que um sistema instÃncia destas regras seja normalizÃvel, definimos um procedimento que normaliza deduÃÃes concretas e comparamos nossas provas de normalizaÃÃo esquemÃtica com provas de normalizaÃÃo para sistemas definidos na literatura. / The term Theory Test was introduced by Hilbert to identify the study of formal proofs. Research in this area can be classified into: a) Proof Theory of reductive or interpretational, whose goal is to demonstrate, among other things, the consistency of mathematics using only methods finitistas, b) Structural Proof Theory, where the structural characteristics of the formal proofs are investigated by means of deductive systems as Natural Deduction and Sequent Calculus. Prawitz through Theory Proof set a Theory of Meaning for constants logics and proposed schematic introduction rules and elimination to characterize the propositional connectives. Schroeder-Heister settings Prawitz extended and formalized the use of rules as hypotheses, making possible the use of separate calculations for assumptions of calculations for logical constants. We are not interested in the investigation of schematic rules to give meaning to the logical constants. We intend to actually set schematic standardization procedures, based on such schematic rules? Attic, in order to identify sufficient conditions for a system to be normalizÃvel. These results are relevant to the Abstract Theory of Evidence, a term used to identify the study of the conditions abstract and general to the proof-theoretical analysis of formal systems. Abstract Theory of Evidence do not study specific logical calculations, but families of calculations instances of rules schematic. Our proposal is therefore based on rules schematic rules can be instantiated for concrete, in particular, by introducing rules modal operators. We prove also theorems NormalizaÃÃoo Weak and Strong systems defined in schematic funÃÃoo schematic of our rules, we obtain sufficient conditions for a system instance is normalizÃvel these rules, we define a procedure that normalizes deductions concrete evidence and compare our standards with evidence schematic standards for systems defined in the literature.

In 2020 Parusiński and Rond proved that every algebraic set X ⊂ R^n is homeomorphic to an algebraic set X’ ⊂ R^n which is described globally (and also locally) by polynomial equations whose coefficients are real algebraic numbers. In general, the following problem was widely open: Open Problem. Is every real algebraic set homeomorphic to a real algebraic set defined by polynomial equations with rational coefficients? The aim of my PhD thesis is to provide classes of real algebraic sets that positively answer to above Open Problem. In Chapter 1 I introduce a new theory of real and complex algebraic geometry over subfields recently developed by Fernando and Ghiloni. In particular, the main notion to outline is the so called R|Q-regularity of points of a Q-algebraic set X ⊂ R^n. This definition suggests a natural notion of a Q-nonsingular Q-algebraic set X ⊂ R^n. The study of Q-nonsingular Q-algebraic sets is the main topic of Chapter 2. Then, in Chapter 3 I introduce Q-algebraic approximation techniques a là Akbulut-King developed in collaboration with Ghiloni and the main consequences we proved, that are, versions ‘over Q’ of the classical and the relative Nash-Tognoli theorems. Last results can be found in in Chapters 3 & 4, respectively. In particular, we obtained a positive answer to above Open Problem in the case of compact nonsingular algebraic sets. Then, after extending ‘over Q’ the Akbulut-King blowing down lemma, we are in position to give a complete positive answer to above Open Problem also in the case of compact algebraic sets with isolated singularities in Chapter 4. After algebraic Alexandroff compactification, we obtained a positive answer also in the case of non-compact algebraic sets with isolated singularities. Other related topics are investigated in Chapter 4 such as the existence of Q-nonsingular Q-algebraic models of Nash manifolds over every real closed field and an answer to the Q-algebrization problem for germs of an isolated algebraic singularity. Appendices A & B contain results on Nash approximation and an evenness criterion for the degree of global smoothings of subanalytic sets, respectively.

Very few standards exist for tting products to people. Footwear fit is a noteworthy example for consumer consideration when purchasing shoes. As a result, footwear manufacturing industry for achieving commercial success encountered the problem of developing right footwear which is fulfills consumer's requirement better than it's competeries. Mass customization starts with understanding individual customer's requirement and it finishes with fulllment process of satisfying the target customer with near mass production efficiency. Unlike any other consumer product, personalized footwear or the matching of footwear to feet is not easy if delivery of discomfort is predominantly caused by pressure induced by a shoe that has a design unsuitable for that particular shape of foot. Footwear fitter have been using manual measurement for a long time, but the combination of 3D scanning systems with mathematical technique makes possible the development of systems, which can help in the selection of good footwear for a given customer. This thesis, provides new approach for addressing the computerize footwear fit customization in industry problem. The design of new shoes starts with the design of the new shoe last. A shoe last is a wooden or metal model of human foot on which shoes are shaped. Despite the steady increase in accuracy, most available scanning techniques cause some deficiencies in the point cloud and a set of holes in the triangle meshes. Moreover, data resulting from 3D scanning are given in an arbitrary position and orientation in a 3D space. To apply sophisticated modeling operations on these data sets, substantial post-processing is usually required. We described a robust algorithm for filling holes in triangle mesh. First, the advance front mesh technique is used to generate a new triangular mesh to cover the hole. Next, the triangles in initial patch mesh is modified by estimating desirable normals instead of relocating them directly. Finally, the Poisson equation is applied to optimize the new mesh. After obtaining complete 3D model, the result data must be generated and aligned before taking this models for shape analysis such as measuring similarity between foot and shoe last data base for evaluating footwear it. Principle Component Analysis (PCA), aligns a model by considering its center of mass as the coordinate system origin, and its principle axes as the coordinate axes. The purpose of the PCA applied to a 3D model is to make the resulting shape independent to translation and rotation asmuch as possible. In analysis, we applied "weighted" PCA instead of applying the PCA in a classical way (sets of 3D point-clouds) for alignment of 3D models. This approach is based on establishing weights associated to center of gravity of triangles. When all of the models are aligned, an efficient algorithm to cut the model to several sections toward the heel and toe for extracting counters is used. Then the area of each contour is calculated and compared with equal sections in shoe last data base for finding best footwear fit within the shoe last data base.