Any form of model-based reasoning is limited by the adherence of the model to the actual reality. Scheduling is the problem of finding a suitable timing to execute a given set of activities accommodating complex temporal constraints. Planning is the problem of finding a strategy for an agent to achieve a desired goal given a formal model of the system and the environment it is immersed in. When time and temporal constraints are considered, the problem takes the name of temporal planning. A common assumption in existing techniques for planning and scheduling is controllability of activities: the agent is assumed to be able to control the timing of starting and ending of each activity. In several practical applications, however, the actual timing of actions is not under direct control of the plan executor. In this thesis, we focus on this temporal uncertainty issue in scheduling and in temporal planning: we propose to natively express temporal uncertainty in the model used for reasoning. We first analyze the state-of-the-art on the subject, presenting a rationalization of existing works. Second, we show how Satisfiability Modulo Theory (SMT) solvers can be exploited to quickly solve different kinds of query in the realm of scheduling under uncertainty. Finally, we address the problem of temporal planning in domains featuring real-time constraints and actions having duration that is not under the control of the planning agent.

Formal methods are becoming increasingly important for debugging and verifying hardware and software systems, whose current complexity makes the traditional approaches based on testing increasingly-less adequate. One of the most promising research directions in formal verification is based on the exploitation of Satisfiability Modulo Theories (SMT) solvers. In this thesis, we present MathSAT, a modern, efficient SMT solver that provides several important functionalities, and can be used as a workhorse engine in formal verification. We develop novel algorithms for two functionalities which are very important in verification -- the extraction of unsatisfiable cores and the generation of Craig interpolants in SMT -- that significantly advance the state of the art, taking full advantage of modern SMT techniques. Moreover, in order to demonstrate the usefulness and potential of SMT in verification, we develop a novel technique for software model checking, that fully exploits the power and functionalities of the SMT engine, showing that this leads to significant improvements in performance.

The lack of generality is a structural weakness of knowledge representation formalisms. Here by lack of generality we mean the inability of any given representation to describe the infinite richness and diversity of the world and also its potentially infinite descriptions which are enabled by language. This lack of generality is the main cause of many of the difficulties encountered so far, just think of the problems which have arisen in the effort of creating reusable ontologies. In this thesis we propose a solution to the problem of generality which is based on the key idea that knowledge should not be modeled a priori, at design time, but it should continuously generated, adapted and evolved, from generation to usage. The thesis provides four main contributions: (i) a shared terminology for the characterization of concepts and for their computational representation; (ii) a formalization of the distinction between substance concepts and classification concepts; (iii) the integration of these two notions of concept into a general representation language that organizes them into a hierarchy of increasing abstraction of what is perceived, and (iv) a two-layered knowledge representation formalism, where the first layer allows to represent concepts, as the main devices for achieving generality, and where the second layer allows to represent concepts as the result of “adapting†a description to the current knowledge representation needs and requirements.

Formal methods are becoming increasingly important for debugging and verifying hardware and software systems, whose current complexity makes the traditional approaches based on testing increasingly-less adequate. One of the most promising research directions in formal verification is based on the exploitation of Satisfiability Modulo Theories (SMT) solvers. In this thesis, we present MathSAT, a modern, efficient SMT solver that provides several important functionalities, and can be used as a workhorse engine in formal verification. We develop novel algorithms for two functionalities which are very important in verification -- the extraction of unsatisfiable cores and the generation of Craig interpolants in SMT -- that significantly advance the state of the art, taking full advantage of modern SMT techniques. Moreover, in order to demonstrate the usefulness and potential of SMT in verification, we develop a novel technique for software model checking, that fully exploits the power and functionalities of the SMT engine, showing that this leads to significant improvements in performance.

Homotopy Type Theory (HoTT) is a quite recent branch of research in mathematical logic, which provides interesting connections among various areas of mathematics. It was first introduced by Vladimir Voevodsky as a means to develop synthetic homotopy theory, and further advancements suggested that it can be used as a formal foundation to mathematics. Among its notable features, inductive and higher inductive types are of great interest, e.g. allowing for the study of geometric entities (such as spheres) in the setting of HoTT. However, so far in most of the literature higher inductive types are treated in an ad-hoc way; there is no easy general schema stating what an higher inductive type is, thus hindering the study of the related proof theory. Moreover, although Martin-Löf Type Theory has been deeply and widely studied, many proof theoretic results about its specific variant used in HoTT are folklore, and the proofs are missing. In this final talk, we provide an overview on some results we obtained, aiming to address these problems. In the first part of the talk, we will discuss a normalization theorem for the type theory underlying HoTT. In the second part of the talk we will propose a general syntax schema to encapsulate a relevant class of higher inductive types, potentially allowing for future study of the proof theory of HoTT enriched with such types.

Fundação de Amparo à Pesquisa do Estado do Rio de Janeiro / Este trabalho apresenta um método para reconhecimento do padrão na biodisponibilidade do ferro, através da interação com substâncias que auxiliam a absorção como vitamina C e vitamina A e nutrientes inibidores como cálcio, fitato, oxalato, tanino e cafeína. Os dados foram obtidos através de inquérito alimentar, almoço e jantar, em crianças de 2 a 5 anos da única Creche Municipal de Paraty-RJ entre 2007 e 2008. A Análise de Componentes Principais (ACP) foi aplicada na seleção dos nutrientes e utilizou-se o Algoritmo Fuzzy C-Means (FCM) para criar os agrupamentos classificados de acordo com a biodisponibilidade do ferro. Uma análise de sensibilidade foi desenvolvida na tentativa de buscar quantidades limítrofes de cálcio a serem consumidas nas refeições. A ACP mostrou que no almoço os nutrientes que explicavam melhor a variabilidade do modelo foram ferro, vitamina C, fitato e oxalato, enquanto no jantar o cálcio se mostrou eficaz na determinação da variabilidade do modelo devido ao elevado consumo de leite e derivados. Para o almoço, a aplicação do FCM na interação dos nutrientes, notou-se que a ingestão de vitamina C foi determinante na classificação dos grupos. No jantar, a classificação de grupos foi determinada pela quantidade de ferro heme na interação com o cálcio. Na análise de sensibilidade realizada no almoço e no jantar, duas iterações do algoritmo determinaram a interferência total do cálcio na biodisponibilidade do ferro. / This dissertation presents a method for pattern recognition on the bioavailability of iron, through interaction with substances that help the absorption such as vitamin C and vitamin A and inhibitors as calcium, phytate, oxalate, tannin and caffeine. The database was obtained through dietary, lunch and dinner, in children 2-5 years in the Municipal Nursery of Paraty - Rio de Janeiro, between 2007 and 2008. The Principal Component Analysis (PCA) was applied in the selection of nutrients and used the Fuzzy C-Means Algorithm (FCM) to create the groups classified according to the bioavailability of iron. A sensitivity analysis was developed in an attempt to find neighboring amounts of calcium being consumed at meals. The PCA showed that at lunch the nutrients that best explained the variability of the model were iron, vitamin C, phytate and oxalate, while at dinner the calcium was effective in determining the variability of the model due to high consumption of dairy products. For lunch, the application of FCM in the interaction of nutrients, it was noted that the intake of vitamin C was decisive in the classification of groups. At dinner, the classification of groups was determined by the amount of iron in the interaction with calcium. In the sensitivity analysis performed for lunch and dinner, two iterations of the algorithm determined the total interference of calcium on iron bioavailability.

Fundação de Amparo à Pesquisa do Estado do Rio de Janeiro / Este trabalho apresenta um método para reconhecimento do padrão na biodisponibilidade do ferro, através da interação com substâncias que auxiliam a absorção como vitamina C e vitamina A e nutrientes inibidores como cálcio, fitato, oxalato, tanino e cafeína. Os dados foram obtidos através de inquérito alimentar, almoço e jantar, em crianças de 2 a 5 anos da única Creche Municipal de Paraty-RJ entre 2007 e 2008. A Análise de Componentes Principais (ACP) foi aplicada na seleção dos nutrientes e utilizou-se o Algoritmo Fuzzy C-Means (FCM) para criar os agrupamentos classificados de acordo com a biodisponibilidade do ferro. Uma análise de sensibilidade foi desenvolvida na tentativa de buscar quantidades limítrofes de cálcio a serem consumidas nas refeições. A ACP mostrou que no almoço os nutrientes que explicavam melhor a variabilidade do modelo foram ferro, vitamina C, fitato e oxalato, enquanto no jantar o cálcio se mostrou eficaz na determinação da variabilidade do modelo devido ao elevado consumo de leite e derivados. Para o almoço, a aplicação do FCM na interação dos nutrientes, notou-se que a ingestão de vitamina C foi determinante na classificação dos grupos. No jantar, a classificação de grupos foi determinada pela quantidade de ferro heme na interação com o cálcio. Na análise de sensibilidade realizada no almoço e no jantar, duas iterações do algoritmo determinaram a interferência total do cálcio na biodisponibilidade do ferro. / This dissertation presents a method for pattern recognition on the bioavailability of iron, through interaction with substances that help the absorption such as vitamin C and vitamin A and inhibitors as calcium, phytate, oxalate, tannin and caffeine. The database was obtained through dietary, lunch and dinner, in children 2-5 years in the Municipal Nursery of Paraty - Rio de Janeiro, between 2007 and 2008. The Principal Component Analysis (PCA) was applied in the selection of nutrients and used the Fuzzy C-Means Algorithm (FCM) to create the groups classified according to the bioavailability of iron. A sensitivity analysis was developed in an attempt to find neighboring amounts of calcium being consumed at meals. The PCA showed that at lunch the nutrients that best explained the variability of the model were iron, vitamin C, phytate and oxalate, while at dinner the calcium was effective in determining the variability of the model due to high consumption of dairy products. For lunch, the application of FCM in the interaction of nutrients, it was noted that the intake of vitamin C was decisive in the classification of groups. At dinner, the classification of groups was determined by the amount of iron in the interaction with calcium. In the sensitivity analysis performed for lunch and dinner, two iterations of the algorithm determined the total interference of calcium on iron bioavailability.

Submitted by Luanna Matias (lua_matias@yahoo.com.br) on 2015-05-15T18:43:17Z No. of bitstreams: 2 Dissertação - Vitor Rodrigues Braga de Souza - 2014.pdf: 2674878 bytes, checksum: c37a3227405eafd0a6bcd6cdfe2ddf04 (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) / Approved for entry into archive by Luanna Matias (lua_matias@yahoo.com.br) on 2015-05-15T19:28:34Z (GMT) No. of bitstreams: 2 Dissertação - Vitor Rodrigues Braga de Souza - 2014.pdf: 2674878 bytes, checksum: c37a3227405eafd0a6bcd6cdfe2ddf04 (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) / Made available in DSpace on 2015-05-15T19:28:34Z (GMT). No. of bitstreams: 2 Dissertação - Vitor Rodrigues Braga de Souza - 2014.pdf: 2674878 bytes, checksum: c37a3227405eafd0a6bcd6cdfe2ddf04 (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) Previous issue date: 2014-09-26 / In the rst part of this work, we present all conical with their cartesian equations and their graphs. Then, we made an approach to concepts of linear algebra, vector spaces, linear transformations, eigenvalues and eigenvectors in order to build matrices of linear transformations able to rotate, translate or even make these conical shear. Constructed matrices, GeoGebra software for constructing graphs obtained by transformation matrices were used. Besides this geometric part, we discuss the quadratic forms in order to identify a conic analyzing only the coe cients of its quadratic form and the eigenvalues. The end result was an excellent visual material built from software GeoGebra applying the concepts of Linear Algebra. We can not fail to mention that the construction of the taper in GeoGebra techniques that replace the ruler, compass and the string used by the ancient Greeks were implemented. / Na primeira parte desse trabalho, apresentamos todas as cônicas com suas respectivas equações cartesianas e seus respectivos grá cos. Em seguida, zemos uma abordagem de conceitos de Álgebra Linear, espaços vetoriais, transformações lineares, autovalores e autovetores a m de, construir as matrizes de transformações lineares capazes de rotacionar, transladar ou até fazer o cisalhamento destas cônicas. Construídas as matrizes, foi utilizado o software GeoGebra para a construção dos grá cos obtidos pelas matrizes de transformação. Além dessa parte geométrica, abordamos as formas quadráticas no intuito de identi car uma cônica analisando apenas os coe cientes da sua forma quadrática e os autovalores associados. O resultado nal foi um excelente material visual construído a partir do software GeoGebra aplicando os conceitos de Álgebra Linear. Não podemos deixar de citar que foram implementadas técnicas de construção das cônicas no GeoGebra que substituem a régua, o compasso e o barbante utilizados pelos gregos antigos.

Submitted by Cláudia Bueno (claudiamoura18@gmail.com) on 2015-10-26T16:12:34Z No. of bitstreams: 2 Dissertação - Iron Felisberto de Freitas - 2015.pdf: 4566285 bytes, checksum: 347da00cced574440e6a02e8b4ddf92f (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) / Approved for entry into archive by Luciana Ferreira (lucgeral@gmail.com) on 2015-10-27T14:35:43Z (GMT) No. of bitstreams: 2 Dissertação - Iron Felisberto de Freitas - 2015.pdf: 4566285 bytes, checksum: 347da00cced574440e6a02e8b4ddf92f (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) / Made available in DSpace on 2015-10-27T14:35:43Z (GMT). No. of bitstreams: 2 Dissertação - Iron Felisberto de Freitas - 2015.pdf: 4566285 bytes, checksum: 347da00cced574440e6a02e8b4ddf92f (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) Previous issue date: 2015-03-27 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES / This paper addresses the formal-logical construction of number systems from the set of natural numbers to the real numbers. Being the rst of these sets presented by the axioms of Peano (1858 - 1932) and the latter results of Dedekind cuts (1831 - 1916) on the set of rational numbers. The passage the set of natural numbers to the integers and for these the rational is done by equivalence classes. From a historical perspective, in order to do that mathematics could advance, had to migrate from a sense of \reality" to an abstract concept of number not subject to the amount of idea. Since the beginning of this formal-logical construction of number systems it is necessary to use the concept of correspondences between any two non-empty sets. Finally , are also addressed the polynomial functions of 1st and 2nd degrees and the respective charts in orthogonal Cartesian plane. / O presente trabalho aborda a constru c~ao l ogico-formal dos sistemas num ericos desde, o conjunto dos n umeros naturais at e ao dos n umeros reais. Sendo o primeiro destes conjuntos apresentado pelos axiomas de Peano (1858 - 1932), e o ultimo resulta dos cortes de Dedekind (1831 - 1916) sobre ao conjunto dos n umeros racionais. A passagem do conjunto dos n umeros naturais ao dos inteiros e destes ao dos racionais e realizado por classes de equival^encias. Em uma perspectiva hist orica, a m de que, a Matem atica pudesse avan car, era preciso migrar de uma no c~ao de \realidade" para um conceito abstrato de n umero n~ao subordinado a ideia de quantidade. Desde o in cio desta constru c~ao l ogico-formal dos sistemas num ericos faz-se necess ario o uso do conceito de correspond^encias entre dois conjuntos n~ao vazios quaisquer. Por m, s~ao tamb em abordadas as fun c~oes polinomiais de 1o e 2o graus e seus respectivos gr a cos no plano cartesiano ortogonal.

Submitted by Cláudia Bueno (claudiamoura18@gmail.com) on 2015-10-27T16:31:33Z No. of bitstreams: 2 Dissertação - Josemir do Carmo - 2014.pdf: 1438185 bytes, checksum: 0121ad4e67767d76ae218de911170ce4 (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) / Approved for entry into archive by Luciana Ferreira (lucgeral@gmail.com) on 2015-10-28T14:15:42Z (GMT) No. of bitstreams: 2 Dissertação - Josemir do Carmo - 2014.pdf: 1438185 bytes, checksum: 0121ad4e67767d76ae218de911170ce4 (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) / Made available in DSpace on 2015-10-28T14:15:42Z (GMT). No. of bitstreams: 2 Dissertação - Josemir do Carmo - 2014.pdf: 1438185 bytes, checksum: 0121ad4e67767d76ae218de911170ce4 (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) Previous issue date: 2014-07-25 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES / This paper aims to present multiple features favored by Mathematical Modelling: a methodological alternative to teaching, mainly, in Elementary Education, in an attempt to bring the reality of the students to the classroom and this way contribute to their motivation in the study of mathematics. For this study the methodological referrals are shown and some steps to work with Modelling in the classroom are established. It also presents some examples of problems, construction and discussion of mathematical models, developed in the classroom for Elementary Education. Difficulties of intervention found by teachers to deal with the modeling are listed and also the processes of teacher’s training in relation to the Modelling are discussed, advocating that they must support themselves reflexively on the experiences with Modelling in the classroom context. This way some guidelines are proposed for an evaluation in Mathematical Modelling. / Neste trabalho buscou-se apresentar os múltiplos aspectos favorecidos pela Modelagem Matemática: uma alternativa metodológica para o ensino, principalmente, na Educação Básica, na tentativa de aproximar a realidade dos alunos à sala de aula e assim contribuir para motivação dos mesmos no estudo da matemática. Para isto são mostrados os encaminhamentos metodológicos e estabelecem-se algumas etapas para o trabalho com a modelagem em sala de aula. Apresentam-se também alguns exemplos de problemas, construção e discussão de modelos matemáticos desenvolvidos em sala de aula para a Educação Básica. São elencadas as dificuldades de intervenção encontradas pelos professores para trabalharem com modelagem e discutem-se também os processos de formação dos professores em relação à Modelagem, advogando que estas devem se apoiar reflexivamente nas experiências com Modelagem no contexto da sala de aula. Dessa forma, são propostas algumas orientações para a avaliação em Modelagem Matemática.