Lógicas modais têm sido amplamente utilizadas em Ciência da Computação e inteligência artificial. Além disso, aplicações de lógicas modais na representação do conhecimento em sistemas distribuídos e, mais recentemente, em sistemas multiagentes, têm apresentado resultados promissores. No entanto, outros sistemas de prova para estas lógicas que não os sistemas axiomáticos à la Hilbert são raros na literatura. Este trabalho tem como objetivo principal preencher esta lacuna existente na literatura, ao propor um sistema de prova por dedução natural rotulada para lógicas do conhecimento.

O conceito de parcialidade e importante em diversas áreas como a Matemática e a Ciência da Computação; ele pode ser utilizado, por exemplo, para expressar computações que não terminam e para definir funções recursivas parciais. Com rela cão a grafos, categorias de homomorfismos parciais são comuns (por exemplo, em gramáticas de grafos com a técnica de single-pushout). Este trabalho propõe uma abordagem diferente: a parcialidade é usada na estrutura interna dos objetos (não nos morfismos).Istoéfeito utilizando uma extensão do conceito de Categoria das Setas, chamada de Categoria das Setas Parciais. E definida entãoa categoria Grp de grafos parciais(tais que arcos podem possuir ou não vértices de origem e/ou destino) e homomorfismos totais.A generalização deste modelo resulta em categorias de grafos parciais internos.Émostrado que Grp é bicompleta e, se C é um topos, a categoria dos grafos parciais internos a C é cocompleta. Grafos parciais podem ser utilizados para definir modelos computacionais tais como autômatos. Uma categoria de Autômatos Parciais, denominada Autp, é construída a partir da categoria de Grafos Parciais. Usando uma extensão de composição de spans de grafos para autômatos, chamada de Composição de Transições, e possível definir as computações de autômatos. Brevemente, uma composição de transi cões de dois autômatos parciais resulta em um autômato parcial onde cada transição representa um caminho de tamanho dois (entre vértices), tal que a primeira metade é uma transição do primeiro autômato e a segunda metade é uma transição do segundo. É possível compor um autômato consigo mesmo diversas vezes; no caso de n sucessivas composições de transições, pode-se obter as palavras da linguagem aceita pelo autômato que necessitam de n+1 passos de computação nos arcos que não possuem origem e nem destino definidos do autômato parcial resultante.

Na última década muitos esforços têm sido feitos em verificação formal de propriedades de agentes do cálculo-π. Uma dessas propriedades é a equivalência observacional, que serve para determinar se um processo é equivalente a sua especificação. Contudo, a verificação de equivalência observacional não é um problema trivial. A maioria dos algoritmos destinados a verificação de equivalência são baseados na construção de sistemas de transições rotuladas (π-autômatos). O principal problema com essa abordagem é o grande número de estados envolvidos podendo chegar a um número infinito. Montanari e Pistore mostram que é possível gerar π-autômatos finitos para agentes-π e é possível reduzir a quantidade de estados desses π-autômatos, através da identificação dos nomes ativos. Um nome é semanticamente ativo em um agente se ele pode ser executado de forma observável por ele. Este é um trabalho de análise estática, que tem por objetivo coletar os possíveis nomes ativos contidos em expressões-π, utilizando para isso um sistema de tipos. A vantagem da utilização de sistemas de tipos em relação a outras formas de análise estática é que sistemas de tipos são sistemas lógicos, logo as técnicas de prova da lógica podem ser aproveitadas no estudo de propriedades de sistemas de tipos. Além disso sistemas de tipos são definidos através da estrutura sintática de expressões, facilitando assim as provas por indução estrutural. Assim a principal contribuição deste trabalho é a elaboração do Active-Base-π, um sistema de tipos para a coleta de nomes ativos de expressões-π.

Lógicas modais têm sido amplamente utilizadas em Ciência da Computação e inteligência artificial. Além disso, aplicações de lógicas modais na representação do conhecimento em sistemas distribuídos e, mais recentemente, em sistemas multiagentes, têm apresentado resultados promissores. No entanto, outros sistemas de prova para estas lógicas que não os sistemas axiomáticos à la Hilbert são raros na literatura. Este trabalho tem como objetivo principal preencher esta lacuna existente na literatura, ao propor um sistema de prova por dedução natural rotulada para lógicas do conhecimento.

Com o objetivo de desenvolver uma fundamentação teórica para o estudo formal de problemas de otimização NP-difíceis, focalizando sobre as propriedades estruturais desses problemas relacionadas à questão da aproximabilidade, este trabalho apresenta uma abordagem semântica para tratar algumas questões originalmente estudadas dentro da Teoria da Complexidade Computacional, especificamente no contexto da Complexidade Estrutural. Procede-se a uma investigação de interesse essencialmente teórico, buscando obter uma formalização para a teoria dos algoritmos aproximativos em dois sentidos. Por um lado, considera-se um algoritmo aproximativo para um problema de otimização genérico como o principal objeto de estudo, estruturando-se matematicamente o conjunto de algoritmos aproximativos para tal problema como uma ordem parcial, no enfoque da Teoria dos Domínios de Scott. Por outro lado, focaliza-se sobre as reduções entre problemas de otimização, consideradas como morfismos numa abordagem dentro da Teoria das Categorias, onde problemas de otimização e problemas aproximáveis são os objetos das novas categorias introduzidas. Dentro de cada abordagem, procura-se identificar aqueles elementos universais, tais como elementos finitos, objetos totais, problemas completos para uma classe, apresentando ainda um sistema que modela a hierarquia de aproximação para um problema de otimização NP-difícil, com base na teoria categorial da forma. Cada uma destas estruturas matemáticas fornecem fundamentação teórica em aspectos que se complementam. A primeira providencia uma estruturação interna para os objetos, caracterizando as classes de problemas em relação às propriedades de aproximabilidade de seus membros, no sentido da Teoria dos Domínios, enquanto que a segunda caracteriza-se por relacionar os objetos entre si, em termos de reduções preservando aproximação entre problemas, num ponto de vista externo, essencialmente categorial.

Orientador: João Meidanis / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-07-26T09:21:57Z (GMT). No. of bitstreams: 1 Walter_MariaEmiliaMachadoTelles_D.pdf: 18591224 bytes, checksum: ee2c0868f8c73b0bd0e5a28a8cdc1faa (MD5) Previous issue date: 1999 / Resumo: Não informado. / Abstract: Not informed. / Doutorado / Doutor em Ciência da Computação

Os algoritmos baseados no paradigma Simulated Annealing e suas variações são atualmente usados de forma ampla na resolução de problemas de otimização de larga escala. Esta popularidade é resultado da estrutura extremamente simples e aparentemente universal dos algoritmos, da aplicabilidade geral e da habilidade de fornecer soluções bastante próximas da ótima. No início da década de 80, Kirkpatrick e outros apresentaram uma proposta de utilização dos conceitos de annealing (resfriamento lento e controlado de sólidos) em otimização combinatória. Esta proposta considera a forte analogia entre o processo físico de annealing e a resolução de problemas grandes de otimização combinatória. Simulated Annealing (SA) é um denominação genérica para os algoritmos desenvolvidos com base nesta proposta. Estes algoritmos combinam técnicas de busca local e de randomização. O objetivo do presente trabalho é proporcionar um entendimento das características do Simulated Annealing e facilitar o desenvolvimento de algoritmos com estas características. Assim, é apresentado como Simulated Annealing e suas variações estão sendo utilizados na resolução de problemas de otimização combinatória, proposta uma formalização através de um método de desenvolvimento de algoritmos e analisados aspectos de complexidade. O método de desenvolvimento especifica um programa abstrato para um algoritmo Simulated Annealing seqüencial, identifica funções e predicados que constituem os procedimentos deste programa abstrato e estabelece axiomas que permitem a visualização das propriedades que estes procedimentos devem satisfazer. A complexidade do Simulated Annealing é analisada a partir do programa abstrato desenvolvido e de seus principais procedimentos, permitindo o estabelecimento de uma equação genérica para a complexidade. Esta equação genérica é aplicável aos algoritmos desenvolvidos com base no método proposto. Uma prova de correção é apresentada para o programa abstrato e um código exemplo é analisado com relação aos axiomas estabelecidos. O estabelecimento de axiomas tem como propósito definir uma semântica para o algoritmo, o que permite a um desenvolvedor analisar a correção do código especificado para um algoritmo levando em consideração estes axiomas. O trabalho foi realizado a partir de um estudo introdutório de otimização combinatória, de técnicas de resolução de problemas, de um levantamento histórico do uso do Simulated Annealing, das variações em torno do modelo e de embasamentos matemáticos documentados. Isto permitiu identificar as características essenciais dos algoritmos baseados no paradigma, analisar os aspectos relacionados com estas características, como as diferentes formas de realizar uma prescrição de resfriamento e percorrer um espaço de soluções, e construir a fundamentação teórica genérica proposta.

Orientador : João Meidanis / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Matematica, Estatistica e Computação Cientifica / Made available in DSpace on 2018-08-01T14:19:36Z (GMT). No. of bitstreams: 1 Pinto_MarceloCezar_M.pdf: 1999848 bytes, checksum: 7799783942d9c23c9162fd09dd7f0591 (MD5) Previous issue date: 2002 / Resumo: Desde 1953, quando Natson e Crick desvendaram a estrutura do DNA (ácido desoxirribonucleico), a área de Biologia Molecular tem avançado rapidamente. Técnicas que permitem a manipulação de biomoléculas foram criadas e aperfeiçoadas desde então, gerando enormes quantidades de dados. A necessidade de processar estas informações criou um novo campo chamado de Biologia Molecular Computacional, o qual consiste em desenvolver e usar técnicas matemáticas e de computação para ajudar a resolver problemas de Biologia Molecular. Existem problemas desta área relacionados a Comparação de Genomas, que consiste, a grosso modo, em analisar e comparar seqüências de ácidos nucléicos ou aminoácidos entre espécies. A comparação de genomas busca desvendar as relações existentes entre diferentes espécies. A descoberta de genes ou porções semelhantes nos genomas pode indicar proximidade evolutiva ou regiões indispensáveis à existência da vida. Por outro lado, as diferenças podem relacionar o comportamento particular de uma espécie com uma determinada região de seu genoma. Diante destas observações, iniciamos o desenvolvimento de um algoritmo que realiza a comparação sintática de genomas baseado nos trabalhos de Li e colegas, que utilizam a Complexidade de Kolmogorov para medir a distância entre dois genomas. Ao invés de uma medida de distância, o algoritmo proposto indica as regiões similares entre genomas que são consideradas relevantes pelo critério da Complexidade Condicional de Kolmogorov / Abstract: Since 1953, when Watson and Crick discovered the DNA (deoxiribonucleic acid) structure, Molecular Biology has advanced quickly. Techniques were developed and improved to manipulate biomolecules since that, generating huge quantities of data. The need to process this information created a new field called Computational Molecular Biology, which consists in the development and usage of mathematical and computing techniques to solve Molecular Biology problems. There are problems in that are a related to Genome Comparison, which consists, roughly speaking, in analysis and comparison of nucleic acid or aminoacid sequences between species. Genome Comparison tries to reveal existing relationships between species. The discovery of similar genes or pieces in genomes can point out evolutionary proximity or indispensable regions for life existence. Besides, differences can relate the unique behavior of a species with some of its genome regions. Based on these observations, we start the development of an algorithm that makes sintatic genome comparison using some ideas of Li and colleagues. They work with Kolmogorov Complexity to measure the distance between two genomes. Instead of a distance measure, the proposed algorithm shows similar regions that are considered relevant by the Conditional Kolmogorov Complexity criteria / Mestrado / Mestre em Ciência da Computação

Orientador : João Meidanis / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-03T03:12:47Z (GMT). No. of bitstreams: 1 Dias_Zanoni_D.pdf: 6022934 bytes, checksum: 053baf9603cad9a617559145036a6ed2 (MD5) Previous issue date: 2002 / Resumo: Hoje em dia, estão disponíveis, publicamente, uma imensa quantidade de informações genéticas. O desafio atual da Genômica é processar estes dados de forma a obter conclusões biológicas relevantes. Uma das maneiras de estruturar estas informações é através de comparação de genomas, que busca semelhanças e diferenças entre os genomas de dois ou mais organismos. Neste contexto, a área de Rearranjo de Genomas vem recebendo bastante atenção ultimamente. Uma forma de comparar genomas é através da distância de rearranjo, determinada pelo número mínimo de eventos de rearranjo que podem explicar as diferenças entre dois genomas. Os principais estudos em distância de rearranjo envolvem eventos de reversões e transposições. A presente coletânea é composta de oito artigos, contendo vários resultados importantes sobre Rearranjo de Genomas. Estes trabalhos foram apresentados em seis conferências, sendo uma nacional e cinco internacionais. Dois destes trabalhos serão publicados em importantes revistas internacionais e outro foi incluído como um capítulo de um livro. Nossas principais contribuições podem ser divididas em dois grupos: um novo formalismo algébrico e uma série de resultados envolvendo o evento de transposição. A nova teoria algébrica relaciona a teoria de Rearranjo de Genomas com a de grupos de permutações. Nossa intenção foi estabelecer um formalismo algébrico que simplificasse a obtenção de novos resultados, até hoje, muito baseados na construção de diagramas. Estudamos o evento de transposição de várias formas. Além de apresentarmos resultados sobre a distância de transposição entre uma permutação e sua inversa, também estudamos o problema de rearranjo envolvendo transposições e reversões simultaneamente, construindo algoritmos de aproximação e estabelecendo uma conjectura sobre o diâmetro. Usamos o formalismo algébrico para mostrar que é possível determinar a distância de fusão, fissão e transposição em tempo polinomial. Este é o primeiro resultado polinomial conhecido para um problema de rearranjo envolvendo o evento de transposição. Por último, introduzimos dois novos problemas de rearranjo: o problema de distância sintênica envolvendo fusões e fissões, e o problema de transposição de prefixos. Para ambos apresentamos resultados significativos, que avançam o conhecimento na área / Abstract: Nowadays, a huge amount of genetic information is public1y available. Genomic's current challenge is to process this information in order to obtain relevant biological conc1usions. One possible way of structuring this information is through genome comparison, where we seek similarities and differences among the genomes of two or more organisms. In this context, the area of Genome Rearrangements has received considerable attention lately. One way of comparing genomes is given by the rearrangement distance, which is determined by the minimum number of rearrangement events that explain the differences between two genomes. The main studies in rearrangement distance involve reversal and transposition events. The present collection is composed of eight artic1es, containing several important results on Genome Rearrangements. These papers were presented in six conferences, one with Brazilian scope and five with international scope. Two of these works will be published in important international journals, and one other work appeared as a book chapter. Our main contributions can be divided into two groups: a new algebraic formalism and a series of results involving the transposition event. The new algebraic theory relates the genome rearrangement theory to the theory of permutation groups. Our intention was to establish an algebraic formalism that simplifies the creation of new results, up to now excessively based on the construction of diagrams. We studied the transposition event in several ways. Besides presenting results on the transpositions distance between a permutation and its inverse, we also studied the rearrangement problem involving transpositions and reversals simultaneously, constructing approximation algorithms and proposing a conjecture on the diameter. We used the algebraic formalism to show that it is possible to determine the distance of fusion, fission, and transposition in polynomial time. This is the first polynomial time result for a rearrangement problem involving the transposition event. Finally, we introduced two now rearrangement problems: the syntenic distance problem involving fission and fusion, and the prefix transposition problem. For each one of these problems we present significant results, widening the knowledge in this area / Doutorado / Doutor em Ciência da Computação

Orientador: João Meidanis / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Matematica, Estatistica e Computação Cientifica / Made available in DSpace on 2018-08-03T20:15:11Z (GMT). No. of bitstreams: 1 Stecca_FlaviodeFreitas_M.pdf: 2291737 bytes, checksum: 854734e6990e1e125c61b7312d5f1056 (MD5) Previous issue date: 2003 / Resumo: Esta dissertação aborda o problema da coloração de arestas restrito aos grafos indiferença. O teorema de Vizing diz que qualquer grafo pode ter suas arestas coloridas com .6 (G) ou .6( G) + 1 cores. Grafos pertencentes à Classe 1 são os grafos cujo índice cromático (n úmero mínimo de cores suficientes para pintar suas arestas) X' é igual a .6 ( G) . Se X' = .6(G) + 1, o grafo pertence à Classe 2. Um grafo é dito overfull se .6(G) l_J < m, onde nem são o número de vértices e o número de arestas, respectivamente. Grafos neighborhood overfull são grafos que têm um vértice de grau máximo cuja vizinhança induz um subgrafo overfull. Grafos indiferença overfull ou neighborhood overfull pertencem à Classe 2. Apresentaremos uma breve compilação de resultados de pesquisas. Dois destes resultados mostram que grafos indiferença com grau máximo ímpar e grafos indiferença reduzidos pertencem à Classe 1, porém o problema ainda está em aberto para um grafo indiferença qualquer. Abordamos o problema criando um modelo de programação linear para coloração de arestas. Implementamos um gerador que nos permitiu gerar grafos indiferença de dife-rentes estruturas. Estes grafos tiveram suas arestas coloridas através de programação linear. Definimos um tipo especial de grafo indiferença denominado grafo indiferença semi-universal. Criamos um método que permite cobrir um grafo indiferença com grafos indiferença semi-universais. Mostramos que resolver o problema para um grafo indife-rença qualquer equivale a estender certas colorações parciais para um grafo indiferença semi-universal qualquer. Reforçamos a conjectura de que todos os grafos indiferença não neighborhood overfull são Classe 1, através de testes práticos em milhares de grafos indi-ferença / Abstract: This dissertation is on the subject of edge coloring restricted to indifference graphs. Vi-zing's theorem states that any graph can be edge-colored with .6. or .6. + 1 colors. Graphs are said to be Class 1 if their chromatic index (minimum number of colors required to produce an edge-coloring) X ' equals .6.( G). If X ' = .6.( G) + 1 the graph is said to be Class 2. A graph is overfull if .6. (G) l _ J < m, where n and m are the number of vertices and number of edges, respectively. Graphs are said to be neighborhood overfull if they have a maximum-degree vertex whose neighborhood induces an overfull subgraph. Overfull and neighborhood overfull indifference graphs are Class 2. vVe will show a brief compilation of research results. Two of these results show that indifference graphs with odd maximum degree and reduced indifference graphs are Class 1, however the problem is open for a generic interference graph. The approach used for the problem was the creation of a linear programming mo dei for edge coloring. A graph generator program that allowed creation of indifference graphs with different structures was implemented. These graphs were edge colored using linear programming. We defined a special type of graph called semi-universal indifference graph. We created a method for covering an indifference graph with semi-universal indifference graphs. We show that solving the problem for indifference graphs is equivalent to ex-tending a partial edge coloring in a semi-universal indifference graph. We reinforce the conjecture that says that all indifference graphs not neighborhood overfull are Class 1, through practical tests in thousands of indifference graphs / Mestrado / Mestre em Ciência da Computação