Neste trabalho, estudamos algumas formas de combinar sistemas de Lógica Modal, analisando quando a combinação preserva propriedades como correção, completude e decidibilidade. Estendemos um estudo já realizado sobre combinações de sistemas de Lógica Modal Normal para sistemas de Lógica Modal Não-normal. O principal resultado deste trabalho é a preservação de completude da aplicação externa de um sistema de Lógica Modal Não-normal M em um sistema lógico L. Outro resultado importante é um exemplo de interação forte na combinação independente, ou fusão, de dois sistemas de Lógica Modal Não-normal. / In this work, we study a few ways of combining Modal Logic systems, analysing when the combination preserves properties like soundness, completeness and decidability. We extend a study of the combination of Normal Modal Logic systems to Non-normal Modal Logic systems. The main result of this work is the completeness preservation in the external application of a Non-normal Modal Logic system M to a logic system L. Another important result is an example of strong interations arising in the fusion of two Non-normal Modal Logic system.

En el estudio de las álgebras relacionadas a las lógicas no-clásicas, los semirretículos (distributivos) están siempre presentes. Por ejemplo, la semántica algebraica del fragmento{ --;^; T} de la lógica intuicionista modal es la variedad de los semirretículos implicativos, que son una clase especial de semirretículos distributivos. En esta tesis, introducimos y estudiamos la clase de semirretículos distributivos acotados dotados de operadores modales que cumplen con la condición de monotonía. Estudiamos una teoría de representación para estas álgebras usando las extensiones canónicas y desarrollamos una dualidad completa a través de espacios sober. Dichos resultados son aplicables, bajo modificaciones menores, al estudio de los retículos distributivos acotados, los semirretículos implicativos, las álgebras de Heyting y a las álgebras de Boole con operadores monótonos. Mostraremos cómo nuestra dualidad se extiende a algunos casos particulares. En el caso de las álgebras de Boole, nuestra dualidad incluye, como casos particulares, las dadas en [12] y [31]. Las lógicas modales monótonas han surgido en distintas áreas de aplicación, como por ejemplo, asociadas a ciertas sem anticas utilizadas en computación teórica e inteligencia artificial. Usando la dualidad desarrollada, estudiaremos algunas extensiones obtenidas a partir de un sistema deductivo basado en semirretículos con operadores modales monótonos. A estos sistemas deductivos los dotaremos de una semántica de entornos, y nuestro objetivo principal es probar la completitud de estas extensiones con respecto a una clase característica de marcos monótonos. La variedad de las álgebras de Boole con operadores modales monótonos es dualmente equivalente a dos clases de marcos monótonos generales descriptivos. Clarificaremos este fenómeno mostrando que existe una correspondencia biyectiva entre estas dos clases. Hablaremos sobre algunas clases de marcos de entornos monótonos generales, tales como las clases de punto compacto, imagen compacto y marcos monótonos generales repletos, y estudiaremos las relaciones entre ellos. También probaremos que las nociones de marco monótono punto compacto, e imagen compacto se preservan bajo morfismos acotados fuertes. / In the study of algebras related to non-classical logics, (distributive) semilattices are always present in the background. For example, the algebraic semantic of the { --;^; T}fragment of intuitionistic logic is the variety of implicative meetsemilattices, which are distributive semilattices. In this thesis we introduce and study the class of distributive meet-semilattices endowed with monotonic modal operators. We study the representation theory of these algebras using the theory of canonical extensions and we give a topological duality (Stone style) for them. Also, we show how our new duality extends to some particular subclasses. So, most of the results given in this paper are applicable, with minor modi cations, to the study of bounded distributive lattices, implicative semilattices, Heyting algebras, and Boolean algebras with monotonic operators. We note that in the particular case of Boolean algebras our duality yields the duality given in [12] and [31]. Monotone modal logics have emerged in several application areas such as computer science and social choice theory. Using the developed duality, we study some extensions obtained from a semilattice based deductive system with monotonic modal operators. We give neighborhood semantics, and our main objective is to prove completeness with respect to a characteristic classes of monotonic frames. The variety of Boolean algebras with monotonic modal operators is dually equivalent to two classes of descriptive general monotonic frames. We shall clarify this phenomenon showing that there exists a bijective correspondence between these two classes. We shall discuss some classes of general monotonic neighborhood frames, such as the classes of point-compact, image compact and replete general m-frames, and we shall study the relationships between them. We shall also prove that the notions of point-compact, and image-compact monotonic frames are preserved by strong bounded morphisms.

The modal logic S5 gives us a simple technical tool to analyze some main notions from philosophy (e.g. metaphysical necessity and epistemological concepts such as knowledge and belief). Although S5 can be axiomatized by some simple rules, this logic shows some puzzling properties. For example, an interpolation result holds for the propositional version, but this same result fails when we add first-order quantifiers to this logic. In this dissertation, we study the failure of the Definability and Interpolation Theorems for first-order S5. At the same time, we combine the results of justification logic and we investigate the quantified justification counterpart of S5 (first-order JT45). In this way we explore the relationship between justification logic and modal logic to see if justification logic can contribute to the literature concerning the restoration of the Interpolation Theorem. / A lógica modal S5 nos oferece um ferramental técnico para analizar algumas noções filosóficas centrais (por exemplo, necessidade metafísica e certos conceitos epistemológicos como conhecimento e crença). Apesar de ser axiomatizada por princípios simples, esta lógica apresenta algumas propriedades peculiares. Uma das mais notórias é a seguinte: podemos provar o Teorema da Interpolação para a versão proposicional, mas esse mesmo teorema não pode ser provado quando adicionamos quantificadores de primeira ordem a essa lógica. Nesta dissertação vamos estudar a falha dos Teoremas da Definibilidade e da Interpolação para a versão quantificada de S5. Ao mesmo tempo, vamos combinar os resultados da lógica da justificação e investigar a contraparte da versão quantificada de S5 na lógica da justificação (a lógica chamada JT45 de primeira ordem). Desse modo, vamos explorar a relação entre lógica modal e lógica da justificação para ver se a lógica da justificação pode contribuir para a restauração do Teorema da Interpolação.

No campo da dinâmica de estruturas, muitas aplicações têm surgido para modelos de Elementos Finitos. Um modelo representativo do sistema real pode levar a um aumento da eficiência da estrutura e a uma redução das margens de segurança de projeto relacionadas a carregamentos externos. Conseqüentemente, a precisão e confiabilidade destes modelos tornam-se cada vez mais importantes e influenciam diretamente na qualidade da estrutura. O objetivo deste trabalho é apresentar os principais métodos de ajuste de modelos de Elementos Finitos (Finite Element Model Updating) baseados em informações modais, e propor uma nova abordagem para o problema de ajuste através de programação não-linear multi-objetivo. São abordadas desde as análises modais e as formas de avaliar a correlação entre modelos numéricos e experimentais até a aplicação das metodologias de ajuste para tornar o modelo fiel às informações de referência. Também é apresentada uma revisão bibliográfica sobre ajuste de modelos, tratando desde os primeiros métodos de ajuste até os mais usados na atualidade. São apresentados ainda os aspectos fundamentais dos métodos de programação não-linear que, através de formulações multi-objetivo, podem se consolidar como ferramentas bastante eficazes nesta área. Três exemplos numéricos são utilizados para demonstração das metodologias e para avaliar comparativamente o desempenho de alguns métodos de ajuste. Inicialmente foi estudado um exemplo de uma viga simples para aplicação dos principais conceitos. Em seguida, uma estrutura representativa de um avião (GARTEUR SM-AG 19) e um modelo do caixão de uma asa foram escolhidos para os outros dois estudos de caso, devido à grande aplicação que as técnicas de ajuste de modelos encontram na indústria aeroespacial. Os resultados obtidos comprovam o grande potencial das técnicas de ajuste de modelos, propostas neste trabalho, para o desenvolvimento de sistemas estruturais.

A Logica Modal tem sido utilizada em Ciencia da Computacao no tratamento de crencas, conhecimento, processamento de linguagem natural, analise de sistemas distribuidos, verificacao de programas concorrentes e paralelos, e raciocinio temporal. Estas aplicacoes requerem o desenvolvimento de provadores automaticos de teoremas para os sistemas modais utilizados nas suas formalizacoes. Este trabalho nas suas formalizacoes. Este trabalho apresenta a implementacao de um provador de teoremas para o sistema modal S4, denominado ProS4. Utilizam-se os tableaux semanticos de Fitting, sendo introduzidas novas heuristicas e estruturas de dados que fazemo provador ser eficiente, sem perder a decidibilidade. Na verificacao da validade ou nao de uma formula modal, o provador apresenta a demonstracao ou o modelo falsificador da formula em questao. O ProS4 pode ser extendido a Logica Temporal Linear de Programas, atraves da adicao do operador proximo (next) e linearizacao na geracao de novos mundos.

Nas últimas décadas, avanços em tecnologias de geração, coleta e armazenamento de dados têm contribuído para aumentar o tamanho dos bancos de dados nas diversas áreas de conhecimento humano. Este aumento verifica-se não somente em relação à quantidade de amostras de dados, mas principalmente em relação à quantidade de características descrevendo cada amostra. A adição de características causa acréscimo de dimensões no espaço matemático, conduzindo ao crescimento exponencial do hipervolume dos dados, problema denominado “maldição da dimensionalidade”. A maldição da dimensionalidade tem sido um problema rotineiro para cientistas que, a fim de compreender e explicar determinados fenômenos, têm se deparado com a necessidade de encontrar estruturas significativas ocultas, de baixa dimensão, dentro de dados de alta dimensão. Este processo denomina-se redução de dimensionalidade dos dados (RDD). Do ponto de vista computacional, a conseqüência natural da RDD é uma diminuição do espaço de busca de hipóteses, melhorando o desempenho e simplificando os resultados da modelagem de conhecimento em sistemas autônomos de aprendizado. Dentre as técnicas utilizadas atualmente em sistemas autônomos de aprendizado, as redes neurais artificiais (RNAs) têm se tornado particularmente atrativas para modelagem de sistemas complexos, principalmente quando a modelagem é difícil ou quando a dinâmica do sistema não permite o controle on-line. Apesar de serem uma poderosa técnica, as RNAs têm seu desempenho afetado pela maldição da dimensionalidade. Quando a dimensão do espaço de entradas é alta, as RNAs podem utilizar boa parte de seus recursos para representar porções irrelevantes do espaço de busca, dificultando o aprendizado. Embora as RNAs, assim como outras técnicas de aprendizado de máquina, consigam identificar características mais informativas para um processo de modelagem, a utilização de técnicas de RDD frequentemente melhora os resultados do processo de aprendizado. Este trabalho propõe um wrapper que implementa um modelo neural de aprimoramento progressivo para RDD em sistemas autônomos de aprendizado supervisionado visando otimizar o processo de modelagem. Para validar o modelo neural de aprimoramento progressivo, foram realizados experimentos com bancos de dados privados e de repositórios públicos de diferentes domínios de conhecimento. A capacidade de generalização dos modelos criados é avaliada por meio de técnicas de validação cruzada. Os resultados obtidos demonstram que o modelo neural de aprimoramento progressivo consegue identificar características mais informativas, permitindo a RDD, e tornando possível criar modelos mais simples e mais precisos. A implementação da abordagem e os experimentos foram realizados no ambiente Matlab, utilizando o toolbox de RNAs. / In recent decades, advances on data generation, collection and storing technologies have contributed to increase databases size in different knowledge areas. This increase is seen not only regarding samples amount, but mainly regarding dimensionality, i.e. the amount of features describing each sample. Features adding causes dimension increasing in mathematical space, leading to an exponential growth of data hypervolume. This problem is called “the curse of dimensionality”. The curse of dimensionality has been a routine problem for scientists, that in order to understand and explain some phenomena, have faced with the demand to find meaningful low dimensional structures hidden in high dimensional search spaces. This process is called data dimensionality reduction (DDR). From computational viewpoint, DDR natural consequence is a reduction of hypothesis search space, improving performance and simplifying the knowledge modeling results in autonomous learning systems. Among currently used techniques in autonomous learning systems, artificial neural networks (ANNs) have becoming particularly attractive to model complex systems, when modeling is hard or when system dynamics does not allow on-line control. Despite ANN being a powerful tool, their performance is affected by the curse of dimensionality. When input space dimension is high, ANNs can use a significant part of their resources to represent irrelevant parts of input space making learning process harder. Although ANNs, and other machine learning techniques, can identify more informative features for a modeling process, DDR techniques often improve learning results. This thesis proposes a wrapper which implements a Progressive Enhancement Neural Model to DDR in supervised autonomous learning systems in order to optimize the modeling process. To validate the proposed approach, experiments were performed with private and public databases, from different knowledge domains. The generalization ability of developed models is evaluated by means of cross validation techniques. Obtained results demonstrate that the proposed approach can identify more informative features, allowing DDR, and becoming possible to create simpler and more accurate models. The implementation of the proposed approach and related experiments were performed in Matlab Environment, using ANNs toolbox.

A inteligência computacional é considerada por diferentes autores da atualidade como o destino manifesto da Ciência da Computação. A modelagem de diversos aspectos da cognição, tais como aprendizagem e raciocínio, tem sido a motivação para o desenvolvimento dos paradigmas simbólico e conexionista da inteligência artificial e, mais recentemente, para a integração de ambos com o intuito de unificar as vantagens de cada abordagem em um modelo único. Para o desenvolvimento de sistemas inteligentes, bem como para diversas outras áreas da Ciência da Computação, o tempo é considerado como um componente essencial, e a integração de uma dimensão temporal nestes sistemas é fundamental para conseguir uma representação melhor do comportamento cognitivo. Neste trabalho, propomos o SCTL (Sequential Connectionist Temporal Logic), uma abordagem neuro-simbólica para integrar conhecimento temporal, representado na forma de programas em lógica, em redes neurais recorrentes, de forma que a caracterização semântica de ambas representações sejam equivalentes. Além da estratégia para realizar esta conversão entre representações, e da verificação formal da equivalência semântica, também realizamos uma comparação da estratégia proposta com relação a outros sistemas que realizam representação simbólica e temporal em redes neurais. Por outro lado, também descrevemos, de foma algorítmica, o comportamento desejado para as redes neurais geradas, para realizar tanto inferência quanto aprendizagem sob uma ótica temporal. Este comportamento é analisado em diversos experimentos, buscando comprovar o desempenho de nossa abordagem para a modelagem cognitiva considerando diferentes condições e aplicações. / Computational Intelligence is considered, by di erent authors in present days, the manifest destiny of Computer Science. The modelling of di erent aspects of cognition, such as learning and reasoning, has been a motivation for the integrated development of the symbolic and connectionist paradigms of artificial intelligence. More recently, such integration has led to the construction of models catering for integrated learning and reasoning. The integration of a temporal dimension into such systems is a relevant task as it allows for a richer representation of cognitive behaviour features, since time is considered an essential component in intelligent systems development. This work introduces SCTL (Sequential Connectionist Temporal Logic), a neuralsymbolic approach for integrating temporal knowledge, represented as logic programs, into recurrent neural networks. This integration is done in such a way that the semantic characterization of both representations are equivalent. Besides the strategy to achieve translation from one representation to another, and verification of the semantic equivalence, we also compare the proposed approach to other systems that perform symbolic and temporal representation in neural networks. Moreover, we describe the intended behaviour of the generated neural networks, for both temporal inference and learning through an algorithmic approach. Such behaviour is then evaluated by means several experiments, in order to analyse the performance of the model in cognitive modelling under di erent conditions and applications.

A inteligência computacional é considerada por diferentes autores da atualidade como o destino manifesto da Ciência da Computação. A modelagem de diversos aspectos da cognição, tais como aprendizagem e raciocínio, tem sido a motivação para o desenvolvimento dos paradigmas simbólico e conexionista da inteligência artificial e, mais recentemente, para a integração de ambos com o intuito de unificar as vantagens de cada abordagem em um modelo único. Para o desenvolvimento de sistemas inteligentes, bem como para diversas outras áreas da Ciência da Computação, o tempo é considerado como um componente essencial, e a integração de uma dimensão temporal nestes sistemas é fundamental para conseguir uma representação melhor do comportamento cognitivo. Neste trabalho, propomos o SCTL (Sequential Connectionist Temporal Logic), uma abordagem neuro-simbólica para integrar conhecimento temporal, representado na forma de programas em lógica, em redes neurais recorrentes, de forma que a caracterização semântica de ambas representações sejam equivalentes. Além da estratégia para realizar esta conversão entre representações, e da verificação formal da equivalência semântica, também realizamos uma comparação da estratégia proposta com relação a outros sistemas que realizam representação simbólica e temporal em redes neurais. Por outro lado, também descrevemos, de foma algorítmica, o comportamento desejado para as redes neurais geradas, para realizar tanto inferência quanto aprendizagem sob uma ótica temporal. Este comportamento é analisado em diversos experimentos, buscando comprovar o desempenho de nossa abordagem para a modelagem cognitiva considerando diferentes condições e aplicações. / Computational Intelligence is considered, by di erent authors in present days, the manifest destiny of Computer Science. The modelling of di erent aspects of cognition, such as learning and reasoning, has been a motivation for the integrated development of the symbolic and connectionist paradigms of artificial intelligence. More recently, such integration has led to the construction of models catering for integrated learning and reasoning. The integration of a temporal dimension into such systems is a relevant task as it allows for a richer representation of cognitive behaviour features, since time is considered an essential component in intelligent systems development. This work introduces SCTL (Sequential Connectionist Temporal Logic), a neuralsymbolic approach for integrating temporal knowledge, represented as logic programs, into recurrent neural networks. This integration is done in such a way that the semantic characterization of both representations are equivalent. Besides the strategy to achieve translation from one representation to another, and verification of the semantic equivalence, we also compare the proposed approach to other systems that perform symbolic and temporal representation in neural networks. Moreover, we describe the intended behaviour of the generated neural networks, for both temporal inference and learning through an algorithmic approach. Such behaviour is then evaluated by means several experiments, in order to analyse the performance of the model in cognitive modelling under di erent conditions and applications.

Nas últimas décadas, avanços em tecnologias de geração, coleta e armazenamento de dados têm contribuído para aumentar o tamanho dos bancos de dados nas diversas áreas de conhecimento humano. Este aumento verifica-se não somente em relação à quantidade de amostras de dados, mas principalmente em relação à quantidade de características descrevendo cada amostra. A adição de características causa acréscimo de dimensões no espaço matemático, conduzindo ao crescimento exponencial do hipervolume dos dados, problema denominado “maldição da dimensionalidade”. A maldição da dimensionalidade tem sido um problema rotineiro para cientistas que, a fim de compreender e explicar determinados fenômenos, têm se deparado com a necessidade de encontrar estruturas significativas ocultas, de baixa dimensão, dentro de dados de alta dimensão. Este processo denomina-se redução de dimensionalidade dos dados (RDD). Do ponto de vista computacional, a conseqüência natural da RDD é uma diminuição do espaço de busca de hipóteses, melhorando o desempenho e simplificando os resultados da modelagem de conhecimento em sistemas autônomos de aprendizado. Dentre as técnicas utilizadas atualmente em sistemas autônomos de aprendizado, as redes neurais artificiais (RNAs) têm se tornado particularmente atrativas para modelagem de sistemas complexos, principalmente quando a modelagem é difícil ou quando a dinâmica do sistema não permite o controle on-line. Apesar de serem uma poderosa técnica, as RNAs têm seu desempenho afetado pela maldição da dimensionalidade. Quando a dimensão do espaço de entradas é alta, as RNAs podem utilizar boa parte de seus recursos para representar porções irrelevantes do espaço de busca, dificultando o aprendizado. Embora as RNAs, assim como outras técnicas de aprendizado de máquina, consigam identificar características mais informativas para um processo de modelagem, a utilização de técnicas de RDD frequentemente melhora os resultados do processo de aprendizado. Este trabalho propõe um wrapper que implementa um modelo neural de aprimoramento progressivo para RDD em sistemas autônomos de aprendizado supervisionado visando otimizar o processo de modelagem. Para validar o modelo neural de aprimoramento progressivo, foram realizados experimentos com bancos de dados privados e de repositórios públicos de diferentes domínios de conhecimento. A capacidade de generalização dos modelos criados é avaliada por meio de técnicas de validação cruzada. Os resultados obtidos demonstram que o modelo neural de aprimoramento progressivo consegue identificar características mais informativas, permitindo a RDD, e tornando possível criar modelos mais simples e mais precisos. A implementação da abordagem e os experimentos foram realizados no ambiente Matlab, utilizando o toolbox de RNAs. / In recent decades, advances on data generation, collection and storing technologies have contributed to increase databases size in different knowledge areas. This increase is seen not only regarding samples amount, but mainly regarding dimensionality, i.e. the amount of features describing each sample. Features adding causes dimension increasing in mathematical space, leading to an exponential growth of data hypervolume. This problem is called “the curse of dimensionality”. The curse of dimensionality has been a routine problem for scientists, that in order to understand and explain some phenomena, have faced with the demand to find meaningful low dimensional structures hidden in high dimensional search spaces. This process is called data dimensionality reduction (DDR). From computational viewpoint, DDR natural consequence is a reduction of hypothesis search space, improving performance and simplifying the knowledge modeling results in autonomous learning systems. Among currently used techniques in autonomous learning systems, artificial neural networks (ANNs) have becoming particularly attractive to model complex systems, when modeling is hard or when system dynamics does not allow on-line control. Despite ANN being a powerful tool, their performance is affected by the curse of dimensionality. When input space dimension is high, ANNs can use a significant part of their resources to represent irrelevant parts of input space making learning process harder. Although ANNs, and other machine learning techniques, can identify more informative features for a modeling process, DDR techniques often improve learning results. This thesis proposes a wrapper which implements a Progressive Enhancement Neural Model to DDR in supervised autonomous learning systems in order to optimize the modeling process. To validate the proposed approach, experiments were performed with private and public databases, from different knowledge domains. The generalization ability of developed models is evaluated by means of cross validation techniques. Obtained results demonstrate that the proposed approach can identify more informative features, allowing DDR, and becoming possible to create simpler and more accurate models. The implementation of the proposed approach and related experiments were performed in Matlab Environment, using ANNs toolbox.

Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, Mestrado em Informática, 2015. / Submitted by Albânia Cézar de Melo (albania@bce.unb.br) on 2015-03-31T15:40:32Z No. of bitstreams: 1 2015_ThiagoCoelhoVieira.pdf: 662085 bytes, checksum: 8fae3df1c74c85937e5cd8c48823b60b (MD5) / Approved for entry into archive by Ruthléa Nascimento(ruthleanascimento@bce.unb.br) on 2015-04-20T19:01:54Z (GMT) No. of bitstreams: 1 2015_ThiagoCoelhoVieira.pdf: 662085 bytes, checksum: 8fae3df1c74c85937e5cd8c48823b60b (MD5) / Made available in DSpace on 2015-04-20T19:01:54Z (GMT). No. of bitstreams: 1 2015_ThiagoCoelhoVieira.pdf: 662085 bytes, checksum: 8fae3df1c74c85937e5cd8c48823b60b (MD5) / Diversos tipos de lógicas são usadas como linguagens para descrever sistemas complexos e suas propriedades com a finalidade de serem verificadas formalmente. Provadores de teoremas baseados em tableaux são ferramentas computacionais capazes de realizar esta tarefa de verificação. Em (WDF98) é proposto um método de prova baseado em tableaux para duas lógicas epistêmico-temporais, KL(n) e BL(n). Neste trabalho implementamos o método de prova baseado em tableaux descrito em (WDF98) e apresentamos um algoritmo para verificação de propriedades epistêmicas e temporais sobre a estrutura do tableau construída por este método. / Logics are used as languages to describe complex systems and their properties in order to be formally verified. Tableaux-based theorem-provers are computational tools which can be used to perform this verification task. (WDF98) propose a proof method based on tableaux for both the epistemic-temporal logics KL(n) and BL(n) . In this work we implement the tableaux-based proof method described in (WDF98) and present an algorithm for verification of epistemic-temporal properties over the structure of the tableau built by this method.