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.

[pt] Cenários de falhas em plataformas offshore constituem riscos ambientais, sociais e econômicos significativos devido à amplitude dos danos que podem ser provocados. Portanto, neste contexto, a adoção de boas práticas de gestão de manutenção é necessária, permitindo a continuidade operacional, através da integridade de ativos. No entanto, há ainda uma necessidade de estudos com uma abordagem holística para uma avaliação multinível de ativos, através de abordagens modernas que mitiguem as limitações da análise de modos e efeitos de falha (FMEA) tradicional. Desse modo, esta pesquisa propõe um framework para a análise FMEA que considera a subjetividade e as importâncias relativas dos critérios de risco, através de uma abordagem integrada que utiliza sistemas hierárquicos de inferência e modelos multicritério, como o Best-Worst Method (BWM) e o fuzzy VIsekriterijumsko KOmpromisno Rangiranje (VIKOR) para fornecer uma classificação estruturada de ativos, orientando o gestor na priorização de manutenção. Esse framework foi validado por meio de um estudo empírico em uma plataforma do tipo Floating Production Storage and Offloading (FPSO), que abordou a problemática da corrosão externa para gestão de manutenção, com base na coleta de dados triangulados. Portanto, a presente pesquisa traz contribuições teóricas ao preencher lacunas através da propositura e aplicação de metodologias integradas, e contribuições práticas ao fornecer aos gestores, responsáveis pela formulação de planos de manutenção, elementos objetivos para uma tomada de decisão mais eficaz, sob o paradigma da confiabilidade. Esse framework pode ser aplicado em outros domínios através do ajuste de critérios avaliativos. / [en] Failure scenarios in offshore platforms pose significant environmental, social, and economic risks due to the magnitude of potential damages they can cause. Therefore, in this context, the adoption of good maintenance management practices is necessary, enabling operational continuity through asset integrity. However, there is still a need for studies with a holistic approach for a multi-level assessment of assets, using modern approaches to mitigate the limitations of traditional Failure Mode and Effects Analysis (FMEA). Thus, this research proposes a framework for FMEA that considers the subjectivity and relative importance of risk criteria, through an integrated approach using hierarchical inference systems and multi-criteria models such as the Best-Worst Method (BWM) and fuzzy VIsekriterijumsko KOmpromisno Rangiranje (VIKOR) to provide a structured classification of assets, guiding managers in maintenance prioritization. This framework was validated through an empirical study on a Floating Production Storage and Offloading (FPSO) platform, addressing the issue of external corrosion for maintenance management, based on triangulated data collection. Therefore, this research brings theoretical contributions by filling gaps through the proposal and application of integrated methodologies, and practical contributions by providing managers responsible for formulating maintenance plans with objective elements for more effective decision-making under the reliability paradigm. This framework can be applied in other domains by adjusting evaluative criteria.

[pt] Garantir que uma base de conhecimento com atos da administração pública contenha apenas fatos em conformidade com sua legislação torna-se um desafio para qualquer gestor público. Para isso, dado o grande volume de dados gerados por empresas públicas, faz-se necessário o emprego de recursos tecnológicos que auxiliem o processo de análise de conformidade destes atos. Este trabalho apresenta uma arquitetura computacional capaz de extrair informações publicados dos diários oficiais e então serializá-los em duas bases de conhecimento: triplas RDF/XML de fatos e triplas de RDF/XML de regras formalizadas em lógica iALC, uma lógica de descrição intuicionista. Para garantir a consistência desta base de conhecimento, foi desenvolvido um SAT Solver para iALC em forma de tableau semântico intuicionista. Uma extensão do tableau intuicionista de primeira ordem apresentado por Fitting (1969). Este SAT Solver faz parte de um módulo que além de gerar modelos e contra-exemplos para as regras formalizadas em iALC, também gera um código preliminar de consultas em SPARQL. Esta abordagem permite inferir e certificar a qualidade dos dados disponíveis na base de conhecimento RDF/XML de fatos. Para garantir a qualidade do nosso SAT Solver, fizemos a prova de soundness das suas regras. Para garantir a qualidade da nossa abordagem lógica, construímos um conjunto de 21 Questões de Competência e aplicamos à nossa ferramenta. Os resultados deste estudo de caso mostraram a eficácia e eficiência da nossa abordagem. / [en] Ensuring that a knowledge base with public administration acts contains only facts in accordance with its legislation becomes a challenge for any public manager. To achieve this, given the large volume of data generated by public companies, it is necessary to apply technological resources that assist in the process of analyzing the compliance of these acts. This work presents a computational architecture capable of extracting information published in official gazettes and then serializing it into two knowledge bases, RDF/XML triples of facts and RDF/XML triples of rules formalized in iALC logic, an intuitionistic description logic. To ensure the consistency of this knowledge base, a SAT Solver for iALC was developed in the form of an intuitionistic semantic tableau. An extension of the first-order intuitionist tableau presented by Fitting (1960). This SAT Solver is part of a module that generates models and counter-examples for rules formalized in iALC and generates a preliminary query code in SPARQL. This approach allows infer and certify the quality of the data available in the RDF/XML knowledge base of facts. To guarantee the quality of our SAT Solver, we carry out the soundness proof of its rules. To ensure the quality of our logical approach, we built a set of 21 Competency Questions and applied our tool. The results of this case study showed our approach s effectiveness and efficiency.

[pt] Este trabalho é uma elaboração, com exemplos, e evolução do Algoritmo de Compressão Horizontal (HC) apresentado e seu Conjunto de Regras de Compressão. Este trabalho apresenta uma prova, feita no Provador Interativo de Teoremas Lean, de que o algoritmo HC pode obter uma Derivação Comprimida, representada por um Grafo Acíclico Dirigido, a partir de qualquer Derivação Tipo-Árvore em Dedução Natural para a Lógica Minimal Puramente Implicacional. Finalmente, a partir da Cobertura e Corretude do algoritmo HC, pode-se argumentar que NP = PSPACE. / [en] This work is an elaboration, with examples, and evolution of the presented Horizontal Compression Algorithm (HC) and its set of Compression Rules. This work argues a proof, done in the Lean Interactive Theorem Prover, that the HC algorithm can obtain a Compressed Derivation, represented by a Directed Acyclic Graph, from any Tree-Like Natural Deduction Derivation in Minimal Purely Implicational Logic. Finally, from the Coverage and Soundness of the HC algorithm, one can argue that NP = PSPACE.

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.

[pt] Esta tese apresenta uma nova metodologia para valoração dinâmica do Capital Intelectual, aplicada ao Capital Humano. Trata-se de oferecer, ao tomador de decisão, uma ferramenta capaz de calcular e comparar o retorno do investimento em ativos intangíveis, como ocorre com outros ativos tangíveis. Através da metodologia proposta, denominada KVA-ACHE, é possível estimar a quantidade potencial de conhecimento humano, utilizado na geração do resultado financeiro da empresa. Essa metodologia também permite medir variações de desempenho nos processos-chave que compõem a cadeia de valor da empresa e o impacto do investimento em educação em um determinado processo. O método KVA-ACHE é composto de cinco módulos, que são executados em três fases. Na primeira fase se avalia a empresa de forma agregada, segundo seu modelo estratégico e, na segunda fase, avalia-se a quantidade de conhecimento potencial e disponível, associado a cada processo-chave. A terceira fase é aplicado o método KVA e obtido o indicador de desempenho ROI. Ao final da sua aplicação, essa metodologia permite: identificar os processos que estão drenando resultado da empresa, através da observação de indicador financeiro adaptado, como o ROIK (Return on Investment on Knowledg), identificar a necessidade individualizada de treinamento para se atingir o máximo de desempenho em um determinado processochave; analisar o impacto percebido em termos percentuais do investimento em educação, realizado em determinado processo-chave; e, finalmente, dar uma visão sobre os recursos de conhecimentos e habilidades disponíveis na equipe de colaboradores, os quais poderão ser aproveitados na avaliação de novos negócios e desafios para empresa. A principal inovação dessa metodologia está no fato de se utilizar a Teoria dos Conjuntos Fuzzy e de Sistemas de Inferência Fuzzy - SIF para transformar conceitos relacionados à disponibilidade e ao uso de conhecimento humano em valores que, dessa forma, permitem a comparação de ativos intangíveis com ativos tangíveis. / [en] This thesis presents a new methodology for dynamic valuation of Intellectual Capital, applied to the Human Capital. It offers, to the decision-maker, a computational tool able to quote and compare the return on investment in intangible assets, as with tangible assets. Through the proposed methodology, called KVAACHE, it is possible to estimate the potential amount of human knowledge, used in generating the company’s financial results. This approach also allows the measurement of variations in performance in the key processes that make up the value chain of the company and the impact of investment in education in a given process. The method KVA-ACHE is composed of five modules, which are executed in three phases. The first phase evaluates the company on an aggregate basis, according to its strategic model, and, in the second phase, the amount of potential and available knowledge, associated with each key process, is evaluated. The third phase applies KVA method. This methodology allows: the identification of the processes that are draining the company’s income by looking at the adapted financial indicators, such as ROIK (Return on Investment on Knowledge); the individualized need for training to achieve maximum performance in a particular key process; the analysis of the impact noticed in terms of percentage of the investment in education, held in a certain key process; and finally, an insight into the resources of knowledge and skills available in the team of collaborators, which may be used in the assessment of new challenges and business to the enterprise. The main innovation of this methodology lies in the use of Fuzzy Set Theory and Fuzzy Inference Systems - FIS to transform concepts related to the availability and use of human knowledge into values, and thus allow the comparison of intangible assets with tangible assets.

[pt] Calibrações manuais periódicas asseguram o funcionamento correto de um instrumento durante certo período de tempo, mas não garantem que sensores defeituosos permaneçam calibrados por outros períodos, além de eventualmente serem desnecessárias. Em plantas industriais, a análise dos sinais fornecidos pelos sensores que monitoram os processos de produção é uma tarefa difícil em virtude da grande dimensão dos dados. Portanto, uma estratégia de monitoramento e correção online para múltiplos sensores se faz necessária. Este trabalho propõe a utilização de dois modelos: um que emprega Redes Neurais Auto-Associativas com Treinamento Robusto Modificado (RNAAM), e outro que emprega o Teste Seqüencial da Razão de Probabilidade (SPRT) e Lógica Fuzzy. Esses modelos são aplicados em um sistema de monitoramento para auto-correção online e auto-validação das medições realizadas por um grande número de sensores. Diferentemente dos modelos existentes, o sistema proposto faz uso de apenas uma RNAAM para reconstruir os sinais dos sensores com falha. Além disso, os estados do sensor e do modelo de auto-correção são validados por meio dos módulos de confiabilidade e de classificação, respectivamente. Para avaliação do modelo, faz-se uso de uma base de dados com medidas de sensores industriais que controlam e realizam o monitoramento de um motor de combustão interna, instalado em um caminhão de mineração. Os resultados obtidos mostram a capacidade do modelo proposto de mapear e corrigir, com um baixo nível de erro, os sinais dos sensores que apresentam falhas, além de fornecer ao especialista uma ferramenta para a realização de cronogramas de revisão de sensores. / [en] Periodical manual calibrations assure the correct operation of an instrument for a certain period of time, but do not guarantee that faulty sensors remain calibrated for other periods, besides being occasionally unnecessary. In industrial plants the analysis of signals from sensors that monitor a plant is a difficult task due to the high-dimensionality of data. Therefore an online strategy for monitoring and correcting multiple sensors is required. This work proposes the use of two models: one that employs Auto Associative Neural Networks with a Modified Robust Training, and another that employs the Sequential Probability Ratio Test (SPRT) and Fuzzy Logic. These models are applied to an online monitoring system for self-correction and selfvalidation of measurements generated by a large number of sensors. Unlike existing models, the proposed system makes use of only one AANN to reconstruct signals from faulty sensors. Moreover, the states of the sensor and of the self correction model are validated through the reliability and classification modules, respectively. The model is evaluated with a database containing measurements of industrial sensors that control and carry out the monitoring of an internal combustion engine installed in a mining truck. Experimental results show the ability of the proposed model to map and correct signals from faulty sensors with a low error, and to provide a tool for sensor review scheduling.

[pt] Segerberg apresentou uma prova geral da completude para lógicas proposicionais. Para tal, um sistema de dedução foi definido de forma que suas regras sejam regras para um operador booleano arbitrário para uma dada lógica proposicional. Cada regra desse sistema corresponde a uma linha na tabela de verdade desse operador. Na primeira parte desse trabalho, mostramos uma extensão da ideia de Segerberg para lógicas proposicionais finito-valoradas e para lógicas não-determinísticas. Mantemos a ideia de definir um sistema de dedução cujas regras correspondam a linhas de tabelas verdade, mas ao invés de termos um tipo de regra para cada valor de verdade da lógica correspondente, usamos uma representação bivalente que usa a técnica de fórmulas separadoras definidas por Carlos Caleiro e João Marcos. O sistema definido possui tantas regras que pode ser difícil trabalhar com elas. Acreditamos que um sistema de cálculo de sequentes definido de forma análoga poderia ser mais intuitivo. Motivados por essa observação, a segunda parte dessa tese é dedicada à definição de uma tradução entre cálculo de sequentes e dedução natural, onde procuramos definir uma bijeção melhor do que as já existentes. / [en] Segerberg presented a general completeness proof for propositional logics. For this purpose, a Natural Deduction system was defined in a way that its rules were rules for an arbitrary boolean operator in a given propositional logic. Each of those rules corresponds to a row on the operator s truth-table. In the first part of this thesis we extend Segerbergs idea to finite-valued propositional logic and to non-deterministic logic. We maintain the idea of defining a deductive system whose rules correspond to rows of truth-tables, but instead of having n types of rules (one for each truth-value), we use a bivalent representation that makes use of the technique of separating formulas as defined by Carlos Caleiro and João Marcos. The system defined has so many rules it might be laborious to work with it. We believe that a sequent calculus system defined in a similar way would be more intuitive. Motivated by this observation, in the second part of this thesis we work out translations between Sequent Calculus and Natural Deduction, searching for a better bijective relationship than those already existing.

Made available in DSpace on 2016-03-22T17:26:43Z (GMT). No. of bitstreams: 1 Gesner.pdf: 787824 bytes, checksum: 39876589a5891eb7dea64c7a471b8166 (MD5) Previous issue date: 2010-12-21 / Traditional digital logic deals with variables assuming only two possible states: false and true. But for a large number of real world modeling, we want intermediary values. The concept of duality, stating that something can and must coexist with its opposite, makes the fuzzy logic seem natural, even inevitable. Thus, the fuzzy logic introduces the ability to infer conclusions and generates responses based on vague information, which is also ambiguous and qualitatively incomplete and inaccurate. In this context, the way of thinking of fuzzy-based systems is similar to humans, representing the expressions of natural language in a very simple and intuitive way, leading to the construction of systems easy to understand and to maintain. Other important area of research based on mathematical models for the treatment of uncertainty considers interval mathematics, which has been applied in the representation of inaccurate data. In interval mathematics, the principle of correctness is the assurance that in the computation of an algorithm, the interval output contains all possible outcomes corresponding to punctual data for an interval input. In addition, the optimality principle, determines that the interval output is the smallest possible one satisfying accuracy. Thus, the correctness is the minimum condition while the optimality is the ideal condition to be satisfied by interval computations. Based on these statements, intervals can be used to represent unknown values and to represent continuous values in scientific computing algorithms. The aims of interval valued fuzzy logic are to consider the interval fuzzy constructions as fuzzy constructors which are correct and to analyze criteria to ensure optimality. The extension of the interval connectives of fuzzy logic in this work is based on the canonical interval representation of real functions and in this case, restricted to the unit interval [0; 1] of the real line. Such representation always returns the smallest interval containing the image of the function. Considering concepts and foundations of both approaches, fuzzy logic and interval mathematics, this work studies the operators defined as coimplications. They are characterized as dual structure of the fuzzy implications. Moreover, it seeks to introduce the extension of the interval fuzzy coimplications, and analyses the satisfaction of properties similar to the respective classes of fuzzy coimplications. In particular, we show that valued interval fuzzy coimplications are representations of fuzzy coimplications satisfying these two principles. This Work also analise the dual structure of interval conjugate fuzzy implications, which are obtained from interval automorphisms / A l´ogica digital tradicional lida com vari´aveis assumindo apenas dois poss´ıveis estados: falso e verdadeiro. Mas para grande n´umero de modelagens do mundo real desejamos valores intermedi´arios. O conceito de dualidade, estabelecendo que algo pode e deve coexistir com o seu oposto, faz a l´ogica difusa parecer natural, at´e mesmo inevit´avel. Assim, a l´ogica fuzzy introduz a habilidade em inferir conclus oes e gerar respostas baseadas em informac¸ oes vagas, amb´ıguas e qualitativamente incompletas e imprecisas. Neste contexto, os sistemas de base fuzzy apresentam uma forma de raciocinar semelhante aos humanos, representando as express oes da linguagem natural de maneira muito simples e intuitiva, levando `a construc¸ ao de sistemas compreens´ıveis e de f´acil manutenc¸ ao. Outra importante ´area de pesquisa baseada em modelos matem´aticos para tratamento da incerteza considera a matem´atica intervalar, a qual vem sendo aplicada na representac¸ ao de dados inexatos. Em matem´atica intervalar, o princ´ıpio da corretude consiste na garantia de que, na computac¸ ao de um algoritmo, a sa´ıda intervalar cont´em todos os poss´ıveis resultados pontuais correspondentes aos dados pontuais referentes `a entrada intervalar. E, o princ´ıpio da optimalidade, determina que a sa´ıda intervalar seja a menor poss´ıvel satisfazendo a corretude. Assim, a corretude ´e a condic¸ ao m´ınima enquanto que a optimalidade ´e a condic¸ ao ideal a ser satisfeita por uma computac¸ ao intervalar. Com base nestes crit´erios, os intervalos podem ser aplicados para representar valores desconhecidos e para representar valores cont´ınuos em algoritmos da Computac¸ ao Cient´ıfica. O principal objetivo da l´ogica fuzzy valorada intervalarmente ´e considerar as construc¸ oes fuzzy intervalares como construc¸ oes fuzzy que s ao corretas e analisar crit´erios que garantam optimalidade. A extens ao intervalar dos conectivos da l´ogica fuzzy em estudo neste trabalho est´a baseada na representac¸ ao intervalar can onica de func¸ oes reais e, neste caso, restrita ao intervalo unit´ario [0; 1] da reta real, que sempre retorna o menor intervalo contendo a imagem da func¸ ao. Consideram-se conceitos e fundamentos de ambas abordagens, da l´ogica fuzzy e da matem´atica intervalar, para estudar os operadores definidos como coimplicac¸ oes, caracterizados como estrutura dual das implicac¸ oes fuzzy, buscando introduzir a extens ao intervalar das coimplicac¸ oes fuzzy, analisando a satisfac¸ ao de propriedades an´alogas `as respectivas classes de coimplicac¸ oes fuzzy valoradas pontualmente. Em particular, mostra-se que coimplicac¸ oes fuzzy valoradas intervalarmente s ao representac¸ oes de coimplicac¸ oes fuzzy satisfazendo estes dois princ´ıpios. O trabalho tamb´em contempla uma an´alise da estrutura dual das conjugadas de implicac¸ oes valoradas intervalarmente, as quais s ao obtidas por ac¸ ao de automorfismos intervalares

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.