Les schématisations de termes permettent de représenter des ensembles infinis de termes ayant une structure similaire de manière finie et compacte. Dans ce travail, nous étudions certains aspects liés à l'utilisation des schématisations de termes en déduction automatique, plus particulièrement dans les méthodes de démonstration de théorèmes du premier ordre par saturation. Après une brève étude comparée des formalismes de schématisation existants, nous nous concentrons plus particulièrement sur les termes avec exposants entiers (ou I-termes). Dans un premier temps, nous proposons une nouvelle approche permettant de détecter automatiquement des régularités dans les espaces de recherche. Cette détection des régularités peut avoir plusieurs applications, notamment la découverte de lemmes nécessaires à la terminaison dans certaines preuves inductives. Nous présentons DS3, un outil qui implémente ces idées. Nous comparons notre approche avec d'autres techniques de généralisation de termes. Notre approche diffère complètement des techniques existantes car d'une part, elle est complètement indépendante de la procédure de preuve utilisée et d'autre part, elle utilise des techniques de généralisation inductive et non déductives. Nous discutons également les avantages et les inconvénients liés à l'utilisation de notre méthode et donnons des éléments informels de comparaison avec les approches existantes. Nous nous intéressons ensuite aux aspects théoriques de l'utilisation des I-termes en démonstration automatique. Nous démontrons que l'extension aux I-termes du calcul de résolution ordonnée est réfutationnellement complète, que l'extension du calcul de superposition n'est pas réfutationnellement complète et nous proposons une nouvelle règle d'inférence pour restaurer la complétude réfutationnelle. Nous proposons ensuite un algorithme d'indexation (pour une sous-classe) des I-termes, utile pour le traitement des règles de simplification et d'élimination de la redondance. Finalement nous présentons DEI, un démonstrateur automatique de théorèmes capable de gérer directement des formules contenant des I-termes. Nous évaluons les performances de ce logiciel sur un ensemble de benchmarks. / Term schematisations allow one to represent infinite sets of terms having a similar structure by a finite and compact form. In this work we study some issues related to the use of term schematisation in automated deduction, in particular in saturation-based first-order theorem proving. After a brief comparative study of existing schematisation formalisms, we focus on terms with integer exponents (or I-terms). We first propose a new approach allowing to automatically detect regularities (obviously not always) on search spaces. This is motivated by our aim at extending current theorem provers with qualitative improvements. For instance, detecting regularities permits to discover lemmata which is mandatory for terminating in some kinds of inductive proofs. We present DS3, a tool which implements these ideas. Our approach departs from existing techniques since on one hand it is completely independent of the proof procedure used and on the other hand it uses inductive generalization techniques instead of deductive ones. We discuss advantages and disadvantages of our method and we give some informal elements of comparison with similar approaches. Next we tackle some theoretical aspects of the use of I-terms in automated deduction. We prove that the direct extension of the ordered resolution calculus is refutationally complete. We provide an example showing that a direct extension of the superposition calculus is not refutationally complete and we propose a new inference rule to restore refutational completeness. We then propose an indexing algorithm for (a subclass of) I-terms. This algorithm is an extension of the perfect discrimination trees that are are employed by many efficient theorem provers to implement redundancy elimination rules. Finally we present DEI, a theorem prover with built-in capabilities to handle formulae containing I-terms. This theorem-prover is an extension of the E-prover developed by S. Schulz. We evaluate the performances of this software on a set of benchmarks.

The goal of General Game Playing (GGP) is to develop a system, that is able to automatically play previously unseen games well, solely by being given the rules of the game. In contrast to traditional game playing programs, a general game player cannot be given game specific knowledge. Instead, the program has to discover this knowledge and use it for effectively playing the game well without human intervention. In this thesis, we present a such a program and general methods that solve a variety of knowledge discovery problems in GGP. Our main contributions are methods for the automatic construction of heuristic evaluation functions, the automated discovery of game structures, a system for proving properties of games, and symmetry detection and exploitation for general games.

Made available in DSpace on 2014-12-17T15:48:07Z (GMT). No. of bitstreams: 1 AntonioAOVS.pdf: 849695 bytes, checksum: 575cdb368ae14f3aad606763ebea7114 (MD5) Previous issue date: 2004-10-13 / The widespread growth in the use of smart cards (by banks, transport services, and cell phones, etc) has brought an important fact that must be addressed: the need of tools that can be used to verify such cards, so to guarantee the correctness of their software. As the vast majority of cards that are being developed nowadays use the JavaCard technology as they software layer, the use of the Java Modeling Language (JML) to specify their programs appear as a natural solution. JML is a formal language tailored to Java. It has been inspired by methodologies from Larch and Eiffel, and has been widely adopted as the de facto language when dealing with specification of any Java related program. Various tools that make use of JML have already been developed, covering a wide range of functionalities, such as run time and static checking. But the tools existent so far for static checking are not fully automated, and, those that are, do not offer an adequate level of soundness and completeness. Our objective is to contribute to a series of techniques, that can be used to accomplish a fully automated and confident verification of JavaCard applets. In this work we present the first steps to this. With the use of a software platform comprised by Krakatoa, Why and haRVey, we developed a set of techniques to reduce the size of the theory necessary to verify the specifications. Such techniques have yielded very good results, with gains of almost 100% in all tested cases, and has proved as a valuable technique to be used, not only in this, but in most real world problems related to automatic verification / O grande crescimento do uso de smart cards (por bancos, companhias de transporte, celulares, etc) trouxe um fato importante, que deve ser considerado: a necessidade de ferramentas que possam ser usadas para verificar os cart?es, para que se possa garantir a corretude de seu software. Como a grande maioria dos cart?es desenvolvidos hoje em dia usa a tecnologia JavaCard em sua camada de software, o uso da Java Modeling Language (JML) para especificar os programas aparece como uma solu?ao natural. JML ? uma linguagem de especifica??o formal ligada ao Java. Ela foi inspirada pelas metodologias de Larch e Eiffel, e foi largamente adotada como a linguagem de facto em se tratando da especifica??o de qualquer programa relacionado ? Java. V?rias ferramentas que fazem uso de JML j? foram desenvolvidas, cobrindo uma grande gama de funcionalidades, entre elas, a verifica??o em tempo de execu??o e est?tica. Mas as ferramentas existentes at? o momento para a verifica??o est?tica n?o s?o totalmente automatizadas, e, aquelas que s?o, n?o oferecem um n?vel adequado de completude e seguran?a. Nosso objetivo ? contribuir com uma s?rie de t?cnicas, que podem ser usadas para alcan?ar uma verifica??o completamente autom?tica e segura para applets JavaCard. Nesse trabalho n?s apresentamos os primeiros passos nessa dire??o. Com o uso de uma plataforma de software composta pelo Krakatoa, Why e haRVey, n?s desenvolvemos um conjunto de t?cnicas para reduzir o tamanho da teoria necess?ria para verificar as especifica??es. Tais t?cnicas deram resultados muito bons, com ganhos de quase 100% em todos os testes que realizamos, e se provou como uma t?cnica que deve ser sempre considerAda, n?o somente nesse, mas na maioria dos problemas reais relacionado com verifica??o autom?tica

In classical propositional logic (CPL) logical reasoning is formalised as logical entailment and can be computed by means of tableau and resolution proof procedures. Unfortunately CPL is not expressive enough and using first order logic (FOL) does not solve the problem either since proof procedures for these logics are not decidable. Modal propositional logics (MPL) on the other hand are both decidable and more expressive than CPL. It therefore seems reasonable to apply tableau and resolution proof systems to MPL in order to compute logical entailment in MPL. Although some of the principles in CPL are present in MPL, there are complexities in MPL that are not present in CPL. Tableau and resolution proof systems which address these issues and others will be surveyed here. In particular the work of Abadi & Manna (1986), Chan (1987), del Cerro & Herzig (1988), Fitting (1983, 1990) and Gore (1995) will be reviewed. / Computing / M. Sc. (Computer Science)

In this dissertation a formalisation of nonmonotonic reasoning, namely Default logic, is discussed. A proof theory for default logic and a variant of Default logic - Prioritised Default logic - is presented. We also pursue an investigation into the relationship between default reasoning and making inferences in a neural network. The inference problem shifts from the logical problem in Default logic to the optimisation problem in neural networks, in which maximum consistency is aimed at The inference is realised as an adaptation process that identifies and resolves conflicts between existing knowledge about the relevant world and external information. Knowledge and data are transformed into constraint equations and the nodes in the network represent propositions and constraint equations. The violation of constraints is formulated in terms of an energy function. The Hopfield network is shown to be suitable for modelling optimisation problems and default reasoning. / Computer Science / M.Sc. (Computer Science)

CAPES / Este trabalho apresenta um estudo sobre os Números Primos que passa por resultados básicos, como a infinitude dos números primos e o Teorema Fundamental da Aritmética, e resultados mais sofisticados, como o Teorema de Wilson e a consequente função geradora de primos. Além dos resultados teóricos apresenta-se uma interpretação geométrica para os números primos. Essa interpretação e aplicada na ilustração de alguns dos resultados relacionados a primos abordados no ensino básico. Atividades envolvendo a interpretação geométrica apresentada são sugeridas no capítulo final. / This work presents a study about Prime Numbers, since basic results, like the prime number’s infinity and the Arithmetic Fundamental Theorem, to more sophisticated results, as Wilson’s Theorem and it’s consequent Prime generating function. Further the theoretical results we present a prime’s geometric interpretation. This interpretation is applied to illustrate some results related to primes, which appears in basic education. Activities about this geometric interpretation are suggested in the final chapter.

Capes / Na busca por uma melhor representação da realidade tridimensional, as Geometrias não- Euclidianas oferecem uma alternativa ao euclidianismo clássico e um dos destaques e a Geometria Projetiva. Assim, o objetivo deste trabalho e, através de ilustrações, contribuir para a assimilação de definições como perspectiva, projeção e o principio da dualidade. E, a partir de resultados importantes como o Teorema de Desargues, o Teorema de Pappus e o Teorema de Pascal, queremos facilitar a compreensão e a visualização de algumas das técnicas de perspectiva que podem ser adaptadas para o uso na sala de aula pelos professores da Educação B ́ sica. A aplicação de uma oficina de Geometria Projetiva em uma turma do 6o ano do Ensino Fundamental e a avaliação dos resultados revelaram que o tema pode ser desenvolvido de maneira promissora com os estudantes na Educação B ́ sica, obtendo uma melhor compreensão do objeto real e associando-o ao conteúdo matemático envolvido. / In search for a better representation of three-dimensional reality, non-Euclidean Geometries offer an alternative to the classic euclidianism and the Projective Geometry is one of the highlights. The purpose of this word is contribute to the assimilation of definitions such as perspective, projection, and the principle of duality, through illustrations. And, from important results as Desargues’ Theorem, Pappus’ Theorem and Pascal’s Theorem, we want to facilitate understanding and viewing some of the perspective techniques that can be adapted for use in classroom by Basic Education teachers. The application of a workshop of Projective Geometry in a class of 6th grade of elementary school and the evaluation of the results revealed that the theme can be developed in a promising way with students in basic education, getting a better comprehension of the real object and associating it to the mathematical content involved.

CAPES / Esta dissertação está dividida em duas partes. A primeira parte é uma introdução da teoria básica de grupos necessária para o desenvolvimento do teorema da órbita-estabilizador, que permite fazer as contagens das simetrias dos poliedros regulares. A segunda parte é a descrição de uma atividade aplicada em sala de aula. / This dissertation is divided in two parts. The first part is an introduction to basic group theory required for the development of the orbit-stabilizer theorem, that allows the counts of symmetries of the regular polyhedra. The second part is the description of an activity applied in classroom.

A Inteligência de Enxame (Swarm Intelligence) é uma área de estudos que busca soluções para problemas de otimização utilizando-se de técnicas computacionais inspiradas no comportamento social emergente encontrado na biologia. A metaheurística Particle Swarm Optimization (PSO) é relativamente nova e foi inspirada no comportamento social de bandos de pássaros. PSO tem apresentado bons resultados em alguns trabalhos recentes de otimização discreta, apesar de ter sido concebido originalmente para a otimização de problemas contínuos. Este trabalho trata o Problema de Atribuição de Tarefas - Task Assignment Problem (TAP), e apresenta uma aplicação: o problema de alocação de táxis e clientes, cujo objetivo da otimização está em minimizar a distância percorrida pela frota. Primeiramente, o problema é resolvido em um cenário estático, com duas versões do PSO discreto: a primeira abordagem é baseada em codificação binária e a segunda utiliza permutações para codificar as soluções. Os resultados obtidos mostram que a segunda abordagem é superior à primeira em termos de qualidade das soluções e tempo computacional, e é capaz de encontrar as soluções ótimas para o problema nas instâncias para as quais os valores ótimos são conhecidos. A partir disto, o algoritmo é adaptado para a otimização do problema em um ambiente dinâmico, com a aplicação de diferentes estratégias de resposta às mudanças. Os novos resultados mostram que a combinação de algumas abordagens habilita o algoritmo PSO a obter boas soluções ao longo da ocorrência de mudanças nas variáveis de decisão problema, em todas as instâncias testadas, com diferentes tamanhos e escalas de mudança. / Swarm Intelligence searches for solutions to optimization problems using computational techniques inspired in the emerging social behavior found in biology. The metaheuristic Particle Swarm Optimization (PSO) is relatively new and can be considered a metaphor of bird flocks. PSO has shown good results in some recent works of discrete optimization, despite it has been originally designed for continuous optimization problems. This paper deals with the Task Assignment Problem (TAP), and presents an application: the optimization problem of allocation of taxis and customers, whose goal is to minimize the distance traveled by the fleet. The problem is solved in a static scenario with two versions of the discrete PSO: the first approach that is based on a binary codification and the second one which uses permutations to encode the solution. The obtained results show that the second approach is superior than the first one in terms of quality of the solutions and computational time, and it is capable of achieving the known optimal values in the tested instances of the problem. From this, the algorithm is adapted for the optimization of the problem in a dynamic environment, with the application of different strategies to respond to changes. The new results show that some combination of approaches enables the PSO algorithm to achieve good solutions along the occurrence of changes in decision variables problem, in all instances tested, with different sizes and scales of change.

Capes / Na busca por uma melhor representação da realidade tridimensional, as Geometrias não- Euclidianas oferecem uma alternativa ao euclidianismo clássico e um dos destaques e a Geometria Projetiva. Assim, o objetivo deste trabalho e, através de ilustrações, contribuir para a assimilação de definições como perspectiva, projeção e o principio da dualidade. E, a partir de resultados importantes como o Teorema de Desargues, o Teorema de Pappus e o Teorema de Pascal, queremos facilitar a compreensão e a visualização de algumas das técnicas de perspectiva que podem ser adaptadas para o uso na sala de aula pelos professores da Educação B ́ sica. A aplicação de uma oficina de Geometria Projetiva em uma turma do 6o ano do Ensino Fundamental e a avaliação dos resultados revelaram que o tema pode ser desenvolvido de maneira promissora com os estudantes na Educação B ́ sica, obtendo uma melhor compreensão do objeto real e associando-o ao conteúdo matemático envolvido. / In search for a better representation of three-dimensional reality, non-Euclidean Geometries offer an alternative to the classic euclidianism and the Projective Geometry is one of the highlights. The purpose of this word is contribute to the assimilation of definitions such as perspective, projection, and the principle of duality, through illustrations. And, from important results as Desargues’ Theorem, Pappus’ Theorem and Pascal’s Theorem, we want to facilitate understanding and viewing some of the perspective techniques that can be adapted for use in classroom by Basic Education teachers. The application of a workshop of Projective Geometry in a class of 6th grade of elementary school and the evaluation of the results revealed that the theme can be developed in a promising way with students in basic education, getting a better comprehension of the real object and associating it to the mathematical content involved.