O aumento da escala e funcionalidade dos sistemas de computação e sua crescente complexidade envolvem um aumento significante de custos e exigem recursos humanos altamente qualificados para o desenvolvimento de software. Integrando-se o uso de métodos formais ao desenvolvimento de sistemas complexos, permite-se realizar análises e verificações destes sistemas, garantindo assim sua correção. Existem diversos formalismos que permitem descrever sistemas, cada qual com diferentes níveis de abstração. Quando consideramos sistemas complexos, surge a necessidade de um modelo que forneça construções abstratas que facilitem o entendimento e a especificação destes sistemas. Um modelo baseado em objetos fornece um nível de abstração que tem sido muito aplicado na prática, onde os dados e os processos que os manipulam são descritos juntos em um objeto. Gramática de Grafos Baseada em Objetos (GGBO) é um modelo baseado em objetos, que além de ser uma linguagem visual, apresenta a vantagem de as especificações adquirirem um estilo baseado em objetos, que é bastante familiar à maioria dos desenvolvedores. Porém, as GGBOs não possuem ainda ferramentas para verificação automática de propriedades desejadas nos sistemas modelados. Uma alternativa para resolver isso é definir uma tradução (que preserve a semântica) desta linguagem para outra, para a qual existam verificadores automáticos. Um formalismo bastante conhecido e estabelecido para descrição de sistemas concorrentes, para o qual existem verificadores automáticos, é o cálculo-π. Porém, sob o aspecto de especificação de sistemas complexos, GGBOs parecem ser mais adequadas como linguagem de especificação que o cálculo-π, pois são visuais, mais intuitivas e possuem um estilo baseado em objetos. Neste trabalho foi definido um formalismo (baseado nas GGBOs), denominado Gramática de Hipergrafos Baseada em Objetos e uma tradução deste formalismo para o cálculo-π, aliando assim as vantagens desses dois métodos. Além disso, para validar a tradução definida, foram feitas provas de que a semântica das gramáticas de hipergrafos baseadas em objetos é preservada na tradução.

Made available in DSpace on 2014-06-12T16:01:12Z (GMT). No. of bitstreams: 2 arquivo7176_1.pdf: 981863 bytes, checksum: b65d9631609e56e387c6959338c69466 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2005 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Os principais métodos da teoria da prova geral são: eliminação-do-corte e normalização. Na teoria da prova há muitos trabalhos voltados ao teorema da eliminação-do-corte para o cálculo de seqüentes clássico. Por outro lado, encontram-se relativamente poucas investigações direcionadas à normalização para a dedução natural clássica. Essa distinção é acentuada quando se tem a normalização para a lógica clássica através de uma estrutura de prova com mais de uma conclusão. Mencionem-se dois autores que apresentam normalização para uma estrutura com mais de uma conclusão, e.g. Ungar e Cellucci. Todavia, nenhuma investigação apresenta um tratamento direcionado às questões inerentes da definição de um procedimento de normalização dentro de uma estrutura de prova com mais de uma conclusão, onde as derivações sejam, de fato, representadas como grafos-de-prova. Portanto, o objetivo central deste trabalho é a definição do procedimento de normalização para os N-Grafos. Os N-Grafos foram definidos por de Oliveira e compõem um sistema de provas simétrico para a dedução natural, onde as regras lógicas e estruturais são apresentadas em uma estrutura de prova com múltipla conclusão e as derivações são representadas como digrafos. Para a definição da normalização dos N-Grafos, foram construídos cinco conjuntos de reduções: lógicas, estruturais, com ciclos, com seqüências de repetição de links e com permutação do enfraquecimento. Essas reduções foram baseadas nos trabalhos de Prawitz, Ungar e Cellucci, bem como, inspiradas pela própria estrutura de grafos-de-prova dos N-Grafos. Ademais, foram definidos o teorema e a prova da normalização, sendo que a prova foi construída de forma direta, em contrapartida à prova indireta de Ungar. Posteriormente, foram estabelecidas as propriedades da terminação e da confluência (fraca) para a normalização dos N-Grafos. Através da construção da normalização para os N-Grafos é possível destacar algumas propostas de trabalhos futuros como, por exemplo, a relação entre provas formais, e processos concorrentes e a investigação da correspondência entre a normalização e a identidade de provas

Made available in DSpace on 2014-06-12T16:01:20Z (GMT). No. of bitstreams: 2 arquivo7782_1.pdf: 981863 bytes, checksum: b65d9631609e56e387c6959338c69466 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2005 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Os principais métodos da teoria da prova geral são: eliminação-do-corte e normalização. Na teoria da prova há diversos trabalhos voltados ao teorema da eliminação-do-corte para o cálculo de sequentes clássico, bem como, investigações direcionadas à normalização para a dedução natural (DN) clássica. Por outro lado, são encontrados poucos trabalhos que buscam definir a normalização para a lógica clássica, através de uma estrutura de prova com mais de uma conclusão. Mencionem-se dois autores que apresentam normalização para uma estrutura com mais de uma conclusão, e.g. Ungar [Ung92] e Cellucci [Cel92]. Todavia, nenhuma investigação apresenta um tratamento direcionado às questões inerentes à definição de um procedimento de normalização dentro de uma estrutura de prova com mais de uma conclusão, onde as derivações sejam, de fato, representadas como grafos-de-prova. Portanto, o objetivo central deste trabalho é a definição do procedimento de normalização para os N-Grafos. Os N-Grafos foram definidos por de Oliveira e compõem um sistema de provas simétrico para a DN, onde as regras lógicas e estruturais são apresentadas em uma estrutura de prova com múltipla conclusão e as derivações são representadas como dígrafos. Para a definição da normalização dos NGrafos, foram construídos cinco conjuntos de reduções: lógicas, estruturais, com ciclos, sequência com repetição de ciclos entrelaçados e permutação do enfraquecimento. Essas reduções foram baseadas nos trabalhos de Prawitz, Ungar e Cellucci, bem como, inspiradas pela própria estrutura de múltipla conclusão dos N-Grafos. Ademais, foram definidos o teorema e a prova da normalização, sendo que a prova foi construída de forma direta, diferentemente da prova indireta dada por Ungar. Posteriormente, foram estabelecidas as propriedades da terminação e da confluência (fraca) para a normalização dos N-Grafos. Através da construção da normalização para os N-Grafos é possível destacar algumas propostas de trabalhos futuros como, por exemplo, a relação entre provas formais e processos concorrentes, e a investigação da correspondência entre a normalização e a identidade de provas

Orientador: Claudina Izepe Rodrigues / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Matematica, Estatistica e Computação Cientifica / Made available in DSpace on 2018-07-26T16:45:39Z (GMT). No. of bitstreams: 1 Colombo_Jones_M.pdf: 6336447 bytes, checksum: 620030ff0cb706f37ef7c0f7947b0631 (MD5) Previous issue date: 2000 / Resumo: Neste trabalho, o objetivo foi o de estudar o problema da reconstrução para torneios com o quociente simples normal. Com este intuito, introduzimos e desenvolvemos no capítulo 1 diversos conceitos, tais como, o quociente de um torneio e mostramos que torneios hipomorfos tais que ambos sejam não simples possuem o mesmo quociente simples. No capítulo 2 introduzimos os conceitos de ciclo minimais e característico. Ao final mostramos que a existência de quociente simples normal é uma propriedade hipomorfa para torneios de ordem superior ou igual a 7. No capítulo 3 demonstramos que os torneios hamiltonianos de ordem maior ou igual a 4 que têm quociente simples normal são reconstrutíveis, se excluirmos um torneio de ordem 5 e dois de ordem 6. Além disso, no início deste capítulo verificamos que os torneios exibidos por Stockmeyer são realmente contra exemplos da conjectura da reconstrução , a qual diz que se dois torneios têm as mesmas cartas são isomorfos. E finalmente apresentamos uma análise das relações entre as classes dos torneios reconstrutíveis atualmente conhecidos(1999). / Abstract: In this work, the objective was to study the reconstruction problem for tournaments with simple normal quotient. With this intention, we introduced and developed in chapter one few concepts, so as, quotient of a tournaments which are not both simple have the same simple quotient. In chapter two we introduce the concepts of minimal and characteristic cycles, and ending this topic we show that the existence of a normal simple quotient is a hipomorphic property for tournaments of order seven or higher. In third chapter we show that hamiltonian tournaments of order four or higher which have normal simple quotient are reconstructible, if we exclude an order five and two of order six tournaments. Moreover, in the beginning of this chapter we check that tour- naments showed by Stockmeyer, be really counterexamples of reconstruction conjecture, which says that if two tournaments with the same cards are isomorphic. Finally we pre-sent and analyse the relation between the reconstruction classes atually known (1999). / Mestrado / Mestre em Matemática

Orientador : Ricardo Dahab / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-07-28T09:27:15Z (GMT). No. of bitstreams: 1 Silva_CandidaNunesda_M.pdf: 9020782 bytes, checksum: 72d783f2186f3848f226c74b427014de (MD5) Previous issue date: 2001 / Mestrado

Orientador: Claudina Izepe Rodrigues / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Matematica, Estatistica e Computação Cientifica / Made available in DSpace on 2018-07-25T18:11:42Z (GMT). No. of bitstreams: 1 Souza_MarcelaLucianoVilelade_M.pdf: 3036170 bytes, checksum: f5c4fa24e4a49364c6bef25d9978950e (MD5) Previous issue date: 1999 / Resumo: Nesta dissertação, o objetivo foi estudar o problema da reconstrução de torneios normais. Para isso, introduzimos primeiro alg,umas noções preliminares sobre a teoria de grafos orientados e torneios. Depois, vimos alguns resultados envolvendo torneios hamiltonianos e bineutros, diferença delica e característica cíelica de um torneio para posteriormente serem aplicados no resultado principal. Finalmente, mostramos os resultados essenciais para o nosso objetivo que estudam a normalidade de torneios hipomorfos e a Composição Canônica do subtorneio Pn-k. / Abstract: Not informed. / Mestrado / Mestre em Matemática

Orientador: Claudina Izepe Rodrigues / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Matematica, Estatistica e Computação Cientifica / Made available in DSpace on 2018-07-31T15:32:01Z (GMT). No. of bitstreams: 1 Santos_ValdomiroPlacidodos_M.pdf: 1319625 bytes, checksum: 58e1f52c8359a65ece38b62fd5fa18a2 (MD5) Previous issue date: 2001 / Resumo: O problema da reconstrução de torneios permanece sem uma conclusão definitiva por aproximadamente quatro décadas. Este trabalho apresenta a evolução das pesquisas sobre este problema e traz também um estudo sobre os torneios de Moon, que constituem uma classe de torneios reconstrutíveis. Em 1966, Frank Harary propôs a seguinte conjectura: todo torneio de ordem n é reconstrutível a partir de suas cartas se n é suficientemente grande. A falsidade desta conjectura (conhecida como conjectura da reconstrução para torneios) foi demonstrada por Stockmeyer, em 1977. Mas, muitas classes de torneios reconstrutíveis foram caracterizadas até o momento. Nosso objetivo neste trabalho é estudar algumas destas classes. Verificamos, na secção 2, que a classe dos torneios não-hamiltonianos constitui uma classe de torneios reconstrutíveis, o que foi provado por Harary e Palmer, em 1967. Centramos nossos estudos, no entanto, na classe dos torneios de Moon, ou seja, os torneios cujos subtorneios ou são hamiltonianos ou são transitivos. Na secção 5, caracterizamos os torneios de Moon por subtorneios transitivos maximais. A partir desta caracterização é possível representar os torneios de Moon pelo seu name . Finalmente, na secção 6, usando o name verificamos que os torneios de Moon são reconstrutíveis a partir de suas cartas / Abstract: The reconstruction problem for tournaments remains without a global solution since 1966. This paper shows the evolution of searches on this problem and presents a study about Moon toumaments, which constitute a class of reconstrutible toumaments. In 1966, Frank Harary posed the reconstrution problem for toumaments by asking: is it possible to reconstruct any toumament To ITom its cards provided n is sufficient1y large? The falsity of the reconstruction conjecture for toumaments was stated by Stockmeyer, in 1977. Several classes of reconstructible toumaments were characterized since the conjecture was posed. The porpose of this paper is to show some of this classes. We verify, in section 2, that the non-hamiltonian toumaments constitute a class of reconstructible toumaments. This result was proved by Harary and Palmer, in 1967. Our main purpose in this paper is to characterize the structure of Moon tournaments, i. e., the toumaments whose subtoumaments are either hamiltonian or transitive. In section 5, we characterize the Moon toumaments by using their maximal transitive subtoumaments. With this new characterization is possible to represent Moon toumaments by using its name. Finely, in section 6, using the name, we prove that Moon toumaments are reconstructible from its cards / Mestrado / Mestre em Matemática

Orientador: Celia Picinin de Mello / Dissertação (mestrado) - Universidade Estadual de Campinas , Instituto de Computação / Made available in DSpace on 2018-07-24T05:57:31Z (GMT). No. of bitstreams: 1 Barbosa_MarceloMarcos_M.pdf: 2201216 bytes, checksum: 6b62fa870c0ee2547c7f2b6fc939b03e (MD5) Previous issue date: 1998 / Resumo: Esta dissertação aborda o assunto Coloração de Arestas (Problema da Classificação) restrita aos cografos, onde o problema está em aberto. Após uma breve compilação de resultados de pesquisas tanto em coloração de arestas como em cografos, encontram-se os resultados obtidos para uma subclasse obtida ao limitarmos o número de níveis da cotree para 3: Ser subgrafo overfull é equivalente a ser overfull ou vizinhança overfull e Algoritmos que colocam na Classe 1 subconjuntos desta subclasse obtidos ao limitarmos o número de ramos da cotree para 2. / Abstract: This dissertation is on the subject of Edge Coloring (Classification Problem) restricted to cographs, for which the problem is open. After a brief compilation of research results on edge coloring and cographs, the results found for a subclass obtained when the number of levels of the cotree is limited to three: Being subgraph overfull is equivalent to being overfull or neighborhood overfull and Algorithms that place into Class 1 some subsets of this subclass obtained when the number of the branches of the cotree is limited to two. / Mestrado / Mestre em Ciência da Computação

Orientador: Claudio L. Lucchesi / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Matematica, Estatistica e Ciencia da Computação / Made available in DSpace on 2018-07-20T10:56:57Z (GMT). No. of bitstreams: 1 Cohen_Jaime_M.pdf: 1980563 bytes, checksum: 88f8b3def82f23368e2850ce7706fb31 (MD5) Previous issue date: 1995 / Resumo: Esta dissertação tem como objetivo apresentar igualdades minimax em grafos que envolvem cortes orientados; cortes ímpares e suas coberturas. A primeira metade da dissertação trata das igualdades que relacionam famílias disjuntas máximas de cortes com as coberturas mínimas dos cortes do grafo. Na segunda parte, os papéis destes problemas são inveI:tidos, isto é, as igualdades relacionam cortes mínimos com famílias disjuntas máximas de coberturas dos cortes. Mostramos ao longo do trabalho que em muitos casos é possível estabelecer analogias entre resultados para cortes orientados e para cortes ímpares. Estas analogias apresentam-se de duas maneiras: através de enunciados semelhantes e através de demonstrações semelhantes. Entre os teoremas apresentados na primeria parte do trabalho, destacam-se os Teoremas de ~ucchesi- Younger e de Edmonds-Giles para cortes orientados e os de Lovász e de Seymour para cortes ímpares. Também são apresentados teoremas que tratam de circuitos orientados e ímpares em grafos planares, mostrando que a analogia também se estende para outros tipos de problemas. Na segunda parte estabelecemos relações entre a igualdade minimax dual ao Teorema de Lovász com a generalização de uma famosa conjectura de Fulkerson. . Provamos um caso particular desta igualdade. Apresentamos também um resultado para um caso particular da igualdade dual ao Teorema de Lucchesi- Younger que foi provado por Schrijver e independentemente por Feofiloff e Younger. / Abstract: The goal of this dissertation is to unify some results of Graph Theory related to directed cuts, odd cuts and their coverings. In the first half of this work we show equalities that relate maximum disjoint families of cuts with the minimum coverings of the cuts of the graph. In the second half, we present the duals of those equalities, i. e., they relate minimum cuts with disjoint families of coverings. Qur main purpose. is to provi de examples that show analogies between results on directed cuts and odd cuts. The analogies are of two types: in the statements of the results and in their proofs. Among the results presented in the first half, the most important are Lucchesi- Younger and Edmonds-Giles' theorems on directed cuts and Lovász and Seymour's theorems for odd cuts. In the last part of this work we extend a result by Seymour that relates the dual of Lovász's theorem with a generalizatión of a famous conjecture due to Fulkerson. We prove a particular case of that equality. We also show an equality for a particular case of the dual of LucchesiYounger's theorem which had been proved by Schrijver and independent1y by Fe,ofiloff and Younger. / Mestrado / Mestre em Ciência da Computação

Diversas são as aplicações que podem ser expressas por meio de grafos [2]. Algoritmos [3] e modelos de visualização [15] podem ser encontrados amplamente na literatura. Todos os problemas de grafos possuem uma base em comum: um modelo genérico que nasce da própria natureza dos elementos e das relações que podem ser expressas entre eles, diferindo apenas pelo tipo de resposta que queremos obter desta complexa malha. Além disso, é natural que, para problemas que sejam de áreas distintas, mas que sejam semelhantes quanto ao processamento interno, apenas o que mude, seja a visualização dos elementos que o compõe (nós, arestas, etc.). Da mesma forma, independente do tipo de processamento interno, os grafos devem manter a estrutura original de grafos, ou seja, ainda deve haver uma malha que descreve os nós e suas ligações. Neste aspecto, fundamentamos nosso estudo: propomos neste trabalho, desenvolver uma API que possa ser estendida para os mais diversos problemas na área de grafos, tanto na parte visual como na representação matemática do modelo e dos algoritmos, porém, robusta, no sentido de manter a complexidade dos algoritmos envolvidos na área de grafos, além de ser completamente dirigida as necessidades de cada aplicação, podendo-se alterar apenas algumas partes da aplicação para obter um produto específico ao trabalho do usuário / There are several applications that can be expressed by means of graphs [2]. Algorithms [3] and visualization models [15] can be widely found in the literature. All graph problems have a common base: create a generic model that arises not only from the nature of their elements, but also from the relationships which these elements can express, differing just by the type of response we want to get from this complex mesh. Moreover, it is natural for problems that are in different fields, but similar in internal processing, that the only change is related to how elements are visualized (nodes, edges, and so on). Likewise, regardless the internal processing, the graphs must keep their original structure, i.e., they must still be a mesh that describes the nodes and their connections. Based on that, this study proposes to develop an API that is generic enough to be extended to several problems in the graphs area. This API can be applied in both visual and mathematical representation of models and algorithms. Besides that, it must be robust to maintain the complexity of the algorithms involved in the graph. Also, it has to be flexible so that only some parts of the application can be changed to get a specific product to the user´s need