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.

[pt] O bairro de Deodoro, localizado na zona oeste da cidade do Rio de Janeiro, é caracterizado por ser um bairro de classe média baixa e por possuir características típicas dos bairros suburbanos da cidade do Rio de Janeiro, como, por exemplo, possuir suas origens muito ligada ao avanço da Estrada de Ferro (ABREU, 2011); Atualmente, o bairro de Deodoro está passando por profundas mudanças em seu espaço em decorrência dos investimentos realizados pelo poder público junto com o capital financeiro para a realização dos Jogos Olímpicos e Paraolímpicos de 2016; Partindo do pressuposto, desenvolvido por Lefebvre (2006) e trabalhado por Carlos (2007; 2011), de que o espaço deve ser compreendido como um produto histórico e social no qual uma sociedade em um determinado momento histórico, através das técnicas que desenvolve e das relações sociais e de produção que estabelece, o produz, esta dissertação se pauta nas múltiplas formas de apropriação e de produção do espaço através da introdução de novos vetores tecnológicos e de investimentos para os Jogos Olímpicos e Paraolímpicos de 2016 nos bairros de Deodoro e da Vila Militar na cidade do Rio de Janeiro e como estas intervenções irão afetar o cotidiano dos moradores do bairro de Deodoro e a sua relação com o bairro vizinho, a Vila Militar; Investigaremos, assim, como o bairro de Deodoro está inserido dentro do contexto da representação da Cidade Olímpica construída pelo poder público e reforçada pela ação da publicidade;. Além disso, chamamos a atenção para as intervenções no espaço destes bairros em decorrência da realização dos Jogos Olímpicos de 2016, como a construção das vias expressas e dos corredores expressos para a circulação do BRT além das arenas esportivas, como o Parque Olímpico de Deodoro, irão transformar a relação dos moradores do bairro de Deodoro com o bairro da Vila Militar. / [en] The Deodoro neighborhood, located in the west of the city of Rio de Janeiro, is characterized by being a lower middle class neighborhood and has characteristics typical of suburban neighborhoods in the city of Rio de Janeiro, for example, has its origins linked to the advancement of the Railroad (ABREU, 2011). Currently, the Deodoro neighborhood is undergoing profound changes in its space as a result of the investments made by the government along with financial capital for the Olympic and Paralympic Games in 2016; Assuming the assumption developed by Lefebvre (2006) and worked for Carlos (2007; 2011) that space must be understood as a historical and social product in which a society at a particular historical moment, through the techniques that develops and social relations and establishing production, produces it, this dissertation is guided in multiple forms of ownership and production of space by introducing new technological vectors and investment for the Olympic and Paralympic Games in 2016 in the districts of Deodoro and Vila Militar in the city of Rio de Janeiro and how these interventions will affect the daily lives of residents of the Deodoro neighborhood and its relationship with the surrounding neighborhood, the Vila Militar; We investigate, as well as the Deodoro neighborhood is inserted into the representation of context Olympic City built by the government and reinforced by action of advertising; In addition, we draw attention to the interventions within these neighborhoods as a result of the Olympic Games in 2016, as the construction of highways and corridors expressed for BRT circulation beyond the sports arenas such as the Olympic Park in Deodoro, will transform the relationship between the residents of the Deodoro neighborhood with the Vila Militar neighborhood.

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.

[pt] Esta dissertação de mestrado apresenta um método para simular cenas de mar para TV/Cinema com um grande número de agentes de vários tipos (embarcações, portos, pessoas, ...) para produções com elevado grau de realismo de imagem e comportamento dos agentes. Este método usa modelagem em lógica nebulosa (fuzzy) e programação no sistema MASSIVE de maneira a integrar os resultados com sistemas de rendering e composição de imagens de alta resolução. Um objetivo importante desta dissertação é criar um sistema que facilita o trabalho de modeladores e designers envolvidos no pipeline de produção. / [en] This MSc dissertation presents a method to simulate sea scenes for TV / Film with a large number of agents of various types (vessels, ports, people ...) for productions with a high degree of realism in both image and agent s behavior. This method uses modeling in fuzzy logic and programming in the MASSIVE system as the main approach to integrate the results with rendering systems and high-resolution images composition. An important goal of this dissertation is to create a system that facilitates the work of modelers and designers involved in the production pipeline.

[pt] As gerações atuais (Y, Z, Me...) são conhecidas como as Gerações Silenciosas pois fazem uso extensivo de mecanismos de mídias sociais e serviços de mensagem (SMS e mais recentemente Whatsapp) em lugar de serviços de voz. Tais gerações, que começam a ser responsáveis por grande parte do mercado consumidor, se sentem mais à vontade com a troca de mensagens vis-à-vis as relações diretas que normalmente ocorrem na comercialização de serviços e suporte pós-venda, facilitando a ampliação do escopo de soluções de auto-serviço e auto-atendimento para esse público. Nesse prisma, torna-se interessante entender de que forma esses novos consumidores se comportam nas mídias sociais e as relações e questões que os levam a adotar novas tecnologias e consumir novos produtos e serviços que podem trazer implicações significativas tanto para a evolução da teoria acadêmica como para gestores de empresas. No presente estudo é proposto um modelo conceitual para avaliação da intenção de adoção de uma nova tecnologia, integrando relações de endosso nas mídias sociais aos efeitos moduladores que o Narcisismo Social (narcisismo nas mídias sociais) podem causar sobre a dimensão afetiva uma vez que o consumo em si não seja uma necessidade fim, mas sim um meio para se auto afirmar. Surveys online com consumidores de serviço de telefonia móvel foram analisados através de equações estruturais afim de se testar se as hipóteses criadas através de indícios de relações observados na revisão da literatura foram ou não confirmadas. / [en] Current generations (Y, Z, Me...) are known as the Silent Generation because they make extensive use of mechanisms of social media and messaging (SMS and more recently Whatsapp) rather than voice services. Such generations, which begin to be responsible for much of the consumer market, feel more comfortable with the message exchange instead of direct relations that normally occur in services commercialization and post-sales support, facilitating the expansion self-service solutions for this public. In this perspective, it is interesting to understand how these new consumers behave in social media and the relationships and issues that lead them to adopt new technologies and consume new products and services that can bring significant implications for the evolution of both academic theory and for managers. In the present study we propose a conceptual model to evaluate the intention to adopt a new technology, integrating the social relations of endorsement to the modulatory effects that social media Narcissism (Narcissism in social media) may have on the affective dimension since consumption itself is not an end but rather a means to assert themselves. Online surveys with mobile phone service consumers were analyzed through structures equation modeling in order to test if the hypotheses created by evidence of the relationships observed in the literature review were confirmed or not.

[pt] É um fato conhecido que provas clássicas podem ser demasiadamente grandes. Estudos em teoria da prova descobriram diferenças exponenciais entre provas normais (ou provas livres do corte) e suas respectivas provas não normais. Por outro lado, provadores automáticos de teorema usualmente se baseiam na construção de provas normais, livres de corte ou provas de corte atômico, pois tais procedimento envolvem menos escolhas. Provas de algumas tautologias são conhecidamente grandes quanto realizadas sem a regra do corte e curtas quando a utilizam. Queremos com este trabalho apresentar procedimentos para reduzir o tamanho de provas proposicionais. Neste sentido, apresentamos dois métodos. O primeiro, denominado método vertical, faz uso de axiomas de extensão e alguns casos é possível uma redução considerável no tamanho da prova. Apresentamos um procedimento que gera tais axiomas de extensão. O segundo, denominado método horizontal, adiciona fórmulas máximas por meio de unificação via substituição de variáveis proposicionais. Também apresentamos um método que gera tal unificação durante o processo de construção da prova. O primeiro método é aplicado a dedução natural enquanto o segundo à Dedução Natural e Cálculo de Seqüentes. As provas produzidas correspondem de certo modo a provas não normais (com a regra do corte). / [en] It is well-known that the size of propositional classical proofs can be huge. Proof theoretical studies discovered exponential gaps between normal or cut-free proofs and their respective non-normal proofs. The task of automatic theorem proving is, on the other hand, usually based on the construction of normal, cut-free or only-atomic-cuts proofs, since this procedure produces less alternative choices. There are familiar tautologies such that the cut-free proof is huge while the non-cut-free is small. The aim of this work is to reduce the weight of proposicional deductions. In this sense we present two methods. The fi first, namely vertical method, uses the extension axioms. We present a method that generates a such extension axiom. The second, namely horizontal method, adds suitable (propositional) unifi fications modulo variable substitutions.We also present a method that generates a such unifi fication during the proving process. The proofs produced correspond in a certain way to non normal proofs (non cut-free proofs).

[pt] A Epistemologia Pós-Darwiniana de Sir Karl Popper é uma tentativa de esclarecer um ponto específico da obra do filósofo austríaco Karl Popper: a função da teoria evolutiva de Charles Darwin na obra epistemológica tardia. Alguns críticos encontram na epistemologia evolucionária, núcleo da obra tardia de Popper, uma virada naturalista baseada na biologia. O principal objetivo dessa dissertação é negar tais interpretações. As bases de aproximação de Popper com o darwinismo em sua epistemologias são lógicas e não naturalísticas. De acordo com Popper, a estrutura lógica do darwinismo ( seus elementos a priori ) é a mesma do processo de conjecturas e refutações do raciocínio dedutivo. Isso explica porquê o darwinismo, que não é uma teoria científica, mas um programa metafísico de pesquisa, pode ser tão frutífero e útil para a ciência. Assim, se estivermos certos, o rótulo de naturalismo aplicado à obra epistemológica tardia de Karl Popper é um simples caso de má interpretação. / [en] The Sir Karl Popper`s PostDarwinian Epistemology intends to clarify an specific issue: the function of Evolutionary Theory by Charles Darwin in Sir Karl Popper`s late epistemological works. Some critics find a naturalistic turn based on biological grounds in the evolutionary epistemology, bulk of the late works of Popper. The main objective of this dissertation is to deny these interpretations. The basis of Popper`s approach to Darwinism in his epistemology is not naturalistic but logical. According to Popper, the logical structure (a priori elements) of Darwinism is the same of conjecture and refutation process of deductive reasoning. This explains why Darwinism, which is not a scientific theory but a metaphysical research program, is so fruitful and helpful to science. Hence, if we are right, the label of naturalism attributed to the late epistemological works of Karl Popper is a simple case of misunderstanding.

[pt] Este trabalho emprega conceitos e ferramentas de Teoria das Categorias e Teoria de Topoi para construir um modelo matemático de problemas, reduções entre problemas, espaços e estratégias de busca heurística. Mais precisamente, uma estratégia de construção de espaços de busca é representada por um funtor de uma certa categoria de problemas para uma certa categoria de florestas. A coleção de todos estes funtores forma um topos, um modelo específico equipado com uma lógica interna própria. Esta lógica interna é usada, então, para definir estratégias de busca e heurísticas em Teoria Local dos Conjuntos. Possíveis aplicações do trabalho incluem (1) a especificação lógica e a classificação de heurísticas e meta-heurísticas usadas na prática e (2) uma versão mais abstrata e geral de resultados específicos relacionando a estrutura de problemas com métodos de resolução adequados. / [en] This work employs concepts and tools from Category Theory and Topos Theory to construct a mathematical model for problems, reductions between problems, heuristic search spaces and strategies. More precisely, a search space construction strategy is represented by a functor from a certain category of problems to a certain category of forests. The collection of all such functors forms a topos, a specific model equipped with its own internal logic. This internal logic is then used to define search satrategies and heuristics in Local Set Theory. Possible applications of this work include (1) the logical specification and classification of heuristics and metaheuristics used in pratice and (2) a more abstract and general rendering of specific results relating the structure of problems to adequate problem-solving methods.

[pt] Assegurar a qualidade de uma avaliação é um grande desafio para os avaliadores. A avaliação de um processo avaliativo denomina-se meta-avaliação. No Brasil já existe uma grande preocupação com a qualidade da avaliação, contudo o conceito de meta-avaliação ainda é uma novidade. Os profissionais discutem quais são os critérios de excelência que uma verdadeira avaliação deve atender tendo como base os padrões definidos pelo Joint Committee on Standards for Educational Evaluation (1994), que estão agrupados em quatro grandes categorias: utilidade, viabilidade, ética e precisão. Este trabalho propõe uma nova metodologia para meta-avaliação utilizando os conceitos de conjuntos fuzzy e da lógica fuzzy. A metodologia é composta por um instrumental de coleta de dados (lista de checagem para meta-avaliação de programas/projetos) e por um sistema de inferência fuzzy hierárquico para o tratamento de dados referentes à metaavaliação de programas/projetos. As principais vantagens de um sistema desse tipo são: (i) a possibilidade de trabalhar com regras lingüísticas; (ii) a utilização de ferramentas adequadas para trabalhar com a imprecisão intrínseca que existe em problemas complexos, como é o caso de processos de meta- avaliação; (iii) a incorporação de conhecimento subjetivo (de especialistas); (iv) a adaptabilidade do processo de inferência a situações específicas. A metodologia ora proposta utiliza um sistema hierárquico composto por trinta e seis bases de regras organizadas em três níveis: padrão (nível 1), categoria (nível 2), e meta-avaliação (nível 3). As principais características da metodologia desenvolvida são: (i) o instrumento de coleta de dados, que permite respostas intermediárias; (ii) a capacidade de adaptação do sistema de inferência fuzzy a necessidades específicas; (iii) a transparência obtida pela utilização de regras lingüísticas, o que facilita a discussão e o entendimento de todo o processo. Acredita-se que esta metodologia facilitará os processos de meta-avaliação. Este estudo pretende ser uma contribuição para a área da avaliação e para a prática da meta-avaliação. / [en] Assuring the quality of an evaluation is a great challenge to evaluators. The evaluation of an evaluative process is called meta- evaluation. In Brazil there is a great concern about evaluation quality, although the concept of metaevaluation is new. Evaluation professionals are still discussing the criteria of excellence that a true evaluation should attend. The standards defined by the Joint Committee on Standards for Educational Evaluation (1994) that are presented in terms of utility, feasibility, ethics and accuracy, enlighten on that discussion. This study presents a new methodology for meta-evaluation that makes use of fuzzy sets and fuzzy logic concepts. The methodology is composed of an instrument for data collection (checklist for the meta-evaluation of programs/projects) and of a hierarchical fuzzy inference system for treatment of data related to the metaevaluation of projects and programs. The main advantages of using such a system are: (i) the possibility of working with linguistic rules; (ii) the use of tools that deal with the intrinsic imprecision of complex problems, as is the case of metaevaluation; (iii) the incorporation of subjective knowledge (of specialists); (iv) the adaptability of the inference process to specific situations. This new methodology makes use of a system composed of 36 rule bases organized in three levels: standard (level 1), category (level 2), and meta- evaluation (level 3). The main features of the proposed methodology are: (i) the data collection instrument, that allows intermediate answers; (ii) the fuzzy system's capability of adaptation to specific needs; (iii) the transparency provided by the use of linguistic rules, which favours understanding and discussion of the whole process. It is believed that this methodology will make the meta-evaluation process easier. This study intends to be a contribution to evaluation as a subject and to meta- evaluation practice.