Álgebra Computacional
Permanent URI for this collection
Browse
Recent Submissions
- Working environment for automated deduction in geometryPublication . Baeta, Nuno Miguel dos Santos; Almeida, Pedro Henrique e Figueiredo Quaresma deGiven its formal, logical and spatial properties, geometry is well suited to be used in teaching environments that include dynamic geometry systems (DGS), geometry automated theorem provers (GATP) and repositories of geometric problems. With the help of the DGS, students can build geometric constructions and conjecture about their properties. With the GATP, students may check the soundness of the constructions (e.g., if two given lines are parallel) and also create formal proofs of conjectures. These tools, backed by repositories of geometric knowledge, provide teachers and students with a framework supported by a large set of geometric constructions and conjectures, for the development of experiments.The ultimate goal is to contribute towards the development of a working environment, where the dynamic geometry component and the automated deduction component work together, providing proofs for plane geometry, in natural language and with a visually dynamic presentation. Quoting Gila Hanna “the best proof is one that also helps understand the meaning of the theorem being proved: to see not only that it is true, but also why it is true”.Building on the work already done in the open source project Open Geometry Prover (OGP), the initial goal was to complete the GATP based on the full-angle method, improving OGP’s library, and allowing the automated deduction in geometry community to profit from a new tool.The OGP project was originally developed by PhD student Ivan Petrović, under the guidance of Predrag Janičić of the University of Belgrade, Serbia, but it was not completed. Having taken over the project, now designated as the Open Geometry Prover Community Project (OGPCP), it was opted for a totally new implementation of a GATP based on the deductive databases for geometry method, having concluded a first version of the automatic theorem prover, the Geometry Deductive Database Prover, fully integrated in the OGPCP.
- Rewriting Prover9Publication . Sousa, Carlos; Araújo, João; Veroff, RobertProver9/Mace4 were the most popular automated theorem provers (ATP) among mathematicians. They had a number of peculiarities that made them especially helpful for research and for teaching. When their author, Bill McCune, died the programs’ destiny was sealed and that was a great loss for many mathematicians throughout the world. The goal of this thesis was to rescue those programs, to add to them new features and to open the gates for many more written in close interaction with professional mathematicians. This project embraces several aspects. The first one was the creation of a translator, an application that allows you to receive a file in Prover9's language as input and translate it into other formats, such as the Waldmeister format or the TPTP format. In this case, The TPTP format allows the translated file to be run by some well-known provers: E-Prover and Vampire. We called this application TranslatorX. Using the translation capability, we have included in this application an algorithm capable of receiving a file in Prover9's language, translating it, and launching, with the same question, all the provers installed on the system that are compatible with the translations. It is also possible to launch Mace4 here, which will try to find a model as a counterexample. The second part of this work was the creation of an application, PortfolioX, which allows proving theorems with several conjectures. However, the great advantage of this application is that it launches several TranslatorX processes, each one with the original axioms and with only one conjecture. As the conjectures are proved one by one, they are added as new axioms, and the process starts again with a stronger axiomatic base, helping to prove the remaining conjectures. In the third phase of this project, we created a graphical application, the Gui application, which included all these processes to help the user enjoy these advantages. We also included in this application the configuration part of the Prover9/PX and Mace4/MX options, which already contain the section to redeclare symbols and their properties. Finally, the code of the Prover9 prover and its base library, LADR, was rewritten in C++ language. Changes were made following suggestions from some Prover9 users, and with this work, we have assimilated greater knowledge of Prover9's algorithms and data structures, which allows us to maintain it, not only in corrective terms but also in terms of improvements and changes.
- Finite model enumerationPublication . Chow, Choiwah; Araújo, João; Janota, Mikoláš; Ferreira, GildaTo study and get intuition on different types of relational algebras (groups, semigroups, and their ordered versions, quasigroups, fields, rings, MV-algebras, lattices, etc.), mathematicians resort to libraries of all models, up to isomorphism, of order n (for small values of n) of the classes of algebras they are interested in. These libraries allow experimentation such as forming and/or testing conjectures etc., to gain insights into the classes of algebras in question. Since an isomorphism partitions the set of all models into equivalence classes, so, only one representative element in each equivalence class is needed. The rest of them are redundant and are removed to make it easy to discern the structure of the algebras. To construct these libraries, we need first to find all models up to isomorphism of the classes of algebras of interest. Enumerating all finite models from first-order formulas up to isomorphism is a hard problem, even for algebras of small orders. The current best practice of finite model enumeration is to divide the job into two steps: first generate models according to the laws laid down by the first-order formula defining the class of algebra, then in the post-processing step, find only one representative model of each equivalence class of isomorphic models. An algebra of finite order n defined by a first-order formula can be represented by operation tables (also known as multiplication tables) of finite sizes. Traditional finite model enumerators such as Mace4 basically perform combinatorial search on these operation tables to find instances that satisfy, or equivalently, not violate, the rules laid down by the first-order formula. This is a hard problem. For example, there are n n 2 possible binary operation tables of size n × n with n possible values in each cell. That is, even to enumerate all models of order 4 defined with just one binary operation in its first-order formula, we are facing the task of checking 4 4 2 ≈ 4.3 billion possibilities. Traditional finite model enumerators also produce a lot of isomorphic models to the extent that isomorphism models often constitute over 99% of the outputs. This is a characteristics of algebras definable by FOL: any permutation on the domain elements of a model is a model. Finding non-isomorphic models is very computationally intensive. If we follow a simple brute-force approach, then, given m models, it may require in the worst case m(m −1)/2 comparisons of models to check for isomorphism. Each comparison of models of order n may require in the worst case n! checks because there are n! different permutations on n symbols. Thus, both of these two steps (generating models from FOL and removing isomorphic models) are resource-intensive. They prompt us to find better algorithms that also make optimal use of the available computing resources. The matter is further complicated by the fact that while modern-day generalpurpose computers are predominantly multi-core, harnessing parallelism for combinatorial search is surprisingly difficult. In this thesis, we propose the isomorphic cubes removal algorithm and the parallel cubes search algorithm to improve the speed of the traditional finite model enumerator. Searching the operation tables can be seen as searching a search tree. Any partial branch from the root (called a cube) can be searched in parallel with other branches, making full use of the computing resources available. Furthermore, some (isomorphic) cubes produce isomorphic models and hence only one of them needs to be searched. Removing isomorphic cubes not only speeds up the search process, but also reduces the number of isomorphic models that need to be removed in the post-processing step. These parallel algorithms are very scalable: more cubes can be generated if more computing resources are available. They also cope with big problems well: longer cubes are possible with higher orders of algebra; with longer cubes, more isomorphic cubes can be removed. To speed up the isomorphic models removal process, we propose the parallel invariant-based isomorphic model removal algorithms. We note that models with different sets of invariant vectors (ordered list of invariants) cannot be isomorphic. We put models into blocks in a hash-table using invariant vectors as the keys. Models across different blocks thus have different sets of invariant vectors and hence cannot be isomorphic. These blocks of models can be checked for isomorphism separately in parallel. The improvement in speed comes from (1) smaller block size means fewer pairs of models to compare for isomorphism, (2) the blocks can be processed in parallel, making full use of the computing resources available. These algorithms also cope with big problems well: models of higher orders give more different invariant vectors to spread out the models. These algorithms together often give an improvement of orders of magnitude in the performance of the traditional finite model enumerators. Better yet, these algorithms can be incorporated in many common finite model enumerators with minimal change in their code base. Furthermore, the proposed algorithms are proved to be correct. In any mathematical research, humans are the most important factor to be given considerations. Not all mathematicians are computer experts, and not all of them want to invest their valuable time in the tools of mathematics. Thus, the tools must be designed to be user-friendly, without a steep learning curve for the user to be able to use the tools effectively. We therefore develop a GAP package generator to automatically generate GAP package for algebras of small orders. The generator hides the technical details of the generation process, but gives users the ability to control many of the non-technical aspects such as the name and the definition (in FOL) of the algebra to be explored. The GAP package generator makes extensive use of the facilities provided by the GAP system, and the generated package complies with the latest GAP standards. A separate, standalone GAP package, Magmaut, is developed to provide functions to manipulate isomorphism and automorphism for algebras of type (2 m, 1 n). It supplements the generated GAP package of algebra of small orders with isomorphism-related functionality. With the tools provided by this project, mathematicians can generate the GAP packages of algebras of type (2 m, 1 n) of their interest, without being bogged down by the complexity that often comes with the tools that generate such GAP packages. In this thesis, we propose many parallel algorithms to take advantage of modern-day multi-core computers to enumerate finite models. We show some important applications of these algorithms in developing GAP packages to calculate different morphisms such as isomorphism and monomorphism etc., in generating GAP packages of algebras, and in counting the number of algebras of small orders. We also develop a user-friendly tool to help mathematicians to generate GAP packages of algebras (of type (2 m, 1 n)) of small orders.
- Forbidden substructure theoremsPublication . Ferreira, Fernando Manuel Maia; Araújo, João; Kinyon, Michael
- Bibliotecas de axiomáticas: conceitos e resultados para sistemas algébricosPublication . Ramires, João Jorge da Costa Vieira; Araújo, João; Matos, David Martins deEm 1996, EQP, um programa de computador, resolveu o Problema de Robbins, um problema colocado nos anos 30 e que tinha derrotado alguns dos maiores algebristas do século XX. Em julho de 2022, Enigma, uma ferramenta de inteligência arti cial aplicada à demonstração automática de teoremas produzida por Josef Urban (Czech Technical University) no âmbito de uma bolsas do Conselho Europeu de Investigação (ERC) que lhe foi concedida para o efeito, demonstrou autonomamente 75% dos teoremas na base de dados Mizar, um repositório contendo grande parte dos teoremas mais comuns, nomeadamente os teoremas lecionados numa licenciatura ou mestrado de matemática pura. Os tempos são de grande mudança e a questão natural é esta: como podemos colocar estas ferramentas a ajudar o progresso da matemática? A resposta que existe hoje consiste em fazer uma pergunta ao computador e ter uma resposta (como aconteceu com o EQP e com a Enigma). Mas será possível desenhar um programa para autonomamente descobrir nova matemática? Aqui há um problema. Já hoje temos computadores capazes de descobrir milhões e milhões de novos teoremas (isto é, sentenças válidas numa determinada teoria) de forma autónoma; mas qual o valor dessa matemática e que impacto tem ou poderá ter? Como garantir que esses teoremas gerados não são triviais, desinteressantes ou inúteis? E o que fazer com teoremas que não se compreendem? Que impacto pode ter imenso ruído ou imensos ininteligíveis? Têm sido avançadas diferentes propostas de resolver a questão natural colocada acima. Algumas delas já revelaram falhar. Outras ainda estão a seguir o seu caminho. O objetivo desta tese é dar uma resposta completamente diferente à pergunta e, como prova de conceito, gerar muitos teoremas, novos, inteligíveis e interessantes. De forma simples (a realidade é bastante mais complexa que a descrição que se segue), a resposta que avançamos nesta tese é a seguinte. Vamos construir um plano em que num dos eixos temos teorias e no outro eixo temos teoremas (ie, sentenças válidas sobre determinados objetos em determinada teoria). No início o nosso plano tem apenas alguns pontos (A, B), signi cando que na teoria A o resultado B é verdadeiro. Por exemplo: Teoria de Grupos, É comutativo o grupo em que cada elemento é inverso de si próprio. Agora, o programa, autonomamente veri ca se (X, B) é verdadeiro (onde B é um teorema conhecido xo e X está a percorrer todas as teorias do nosso repositório). Sempre que encontra uma prova para (Q, B), temos um teorema novo, que é totalmente compreensível e familiar, e que (no caso de Q generalizar A) será tão ou mais interessante que o teorema (A, B) original. Por exemplo, ao correr o nosso programa no repositório, imediatamente surge o teorema: Teoria de Semigrupos Inversos, É comutativo o semigrupo inverso em que cada elemento é inverso de si próprio. Acontece que os grupos são uma pequena classe dentro dos semigrupos inversos, uma estrutura que aparece naturalmente na geometria, e o teorema de grupos referido é dado em qualquer curso de teoria de grupos, enquanto o teorema de semigrupos inversos aparentemente nem sequer aparece na literatura. De igual modo, dado o teorema (A, B), podemos procurar teoremas (A, X), em que X está a percorrer teoremas conhecidos do repositório. No caso de se provar (A, P), teremos um teorema famoso P, até então conhecido para a teoria T, e que agora se veri ca ocorrer na teoria A também. Uma vez mais o resultado é familiar, inteligível e novo. Um utilizador que descobre um teorema T numa axiomática A, pode colocar T no nosso sistema que irá procurar pares (X, T), quando X percorre a base de dados de axiomáticas do nosso repositório. Tendo como resposta (A1, T), (A2, T),..., (An, T), o utilizador cará assim a saber que o seu teorema é um fenómeno muito mais geral e portanto pode procurar uma teoria geral Γ que contenha todas as teorias Ai como casos particulares e na qual o seu teorema T ainda seja verdadeiro. Mais interessante ainda, esta busca da teoria Γ pode ser feita autonomamente pelo computador. De forma análoga, um matemático pode ser levado à introdução de uma nova classe A. O nosso sistema vai procurar pares (A, X), onde X são teoremas na base de dados, pelo que poucos minutos depois de ter identi cado a nova classe, o utilizador poderá já ter vários teoremas familiares, possivelmente não triviais e uma base muito mais sólida para prosseguir a sua investigação. Quando antes a introdução de uma nova classe signi cava o início de um longo e penoso caminho a provar novos teoremas, a início elementares, e depois crescentemente complexos, o nosso sistema permite obter um corpo signi cativo de teoremas, podendo alguns ter provas altamente complexas, não obstante soando familiares e compreensíveis. É esta a resposta que esta tese propõe para a pergunta mais natural do momento: como se pode domar, tornar signi cativa e útil, a capacidade ilimitada de gerar novos teoremas dos computadores?
- Computing congruences and endomorphisms for algebras of type (2m, 1n)Publication . Pereira, Rui Barradas; Araújo, João; Bentz, Wolfram; Sequeira, LuisAtualmente a principal aplicação de software para semigrupos é a package de GAP chamada Semigroups [29], em articulação com a package Smallsemi [13]. O GAP [17] é um sistema e linguagem de programação para álgebra discreta computacional. Embora estas packages ofereçam muitas opções de cálculo e forneçam uma biblioteca de todos os semigrupos até o tamanho 8, várias operações de semigrupos importantes não estão disponíveis. Em parte, isto deve-se ao facto de a arquitetura subjacente ser voltada para a teoria de grupos e os semigrupos frequentemente requerem técnicas algorítmicas que são mais próximas das empregadas na Álgebra Universal do que daquelas usadas em grupos. Existem maneiras de construir álgebras a partir das existentes (produtos diretos etc.), mas a operação inversa é crítica: decompor uma dada álgebra em outras menores. Este tipo de decomposição é especialmente importante em semigrupos, pois mesmo a estrutura de semigrupos muito pequenos pode ser muito obscura. Até agora não existe uma ferramenta computacional geral para decompor semigrupos. Por exemplo, o GAP já contém código para encontrar todas as congruências de classes muito particulares de semigrupos, mas está muito longe de fornecer um método geral. A situação é ainda pior em relação aos endomorfismos. O objetivo da package CREAM (Algebra CongRuences, Endomorphisms and AutomorphisMs) é resolver esta situação implementando algoritmos eficientes para calcular congruências, endomorfismos e automorfismos de álgebras do tipo (2m, 1 n). Vários algoritmos gerais (como em [15]) serão adaptados para o contexto da teoria de semigrupos e mais geralmente para álgebras do tipo (2m, 1 n ) cobrindo assim grupos e semigrupos mas também álgebras unárias e também loops, campos, anéis, semianéis, álgebras de Lie, MV-álgebras, Meadows, álgebras de lógica, etc. Estes algoritmos serão implementados em GAP. Isso incluirá as seguintes questões: • Dada uma álgebra finita A do tipo (2m, 1 n ), encontrar todas as congruências de A, pelo menos tão rápido quanto os programas existentes (ou seja, o código produzido será geral e pelo menos tão rápido quanto o código que existe para classes específicas de álgebras apenas); • Dada uma álgebra finita A do tipo (2m, 1 n ), encontrar todos os endomorfismos de A; em particular, o código deve calcular efetivamente os automorfismos de A, uma ferramenta que essencialmente existe apenas para grupos. Uma álgebra universal é uma estrutura algébrica que consiste num conjunto A e numa coleção de operações sobre A. Uma operação n-aria sobre A é uma função que tem como entrada um n-tuplo de elementos de A e retorna um elemento de A. Neste contexto só estão a ser consideradas operações com aridade 1 ou 2, i.e. operações unárias e binárias. Uma álgebra do tipo (2m, 1 n ) é uma álgebra universal com m operações binárias e n unárias. Este uso genérico da package CREAM depende de teoremas de álgebra universal. Isto tem custos, pois teoremas de tipos específicos de álgebras (e.g. grupos, semigrupos, etc) não podem ser usados para reduzir o espaço de procura e melhorar a performance. Canon e Holt [10], usaram vários algoritmos inteligentes e teoremas específicos de grupos para produzir código mais rápido que a package CREAM a calcular automorfismos de grupos com ordens maiores. Analogamente, Mitchell et al. [29] usaram teoremas da teoria de semigrupos para calcular eficazmente automorfismos e congruências de semigrupos completamente 0-simples. Mas estes estão entre os poucos casos de código GAP disponível que é mais rápido que a package CREAM que é de uso mais generalizado. Para a maioria de outras classes de álgebras de tipo (2m, 1 n ) a package CREAM é mais rápida a calcular auto[endo]morfismos/congruências. Um dos algoritmos principais implementado na package é o algoritmo de Freese descrito em [15] que calcula congruências principais para uma álgebra universal. Para chegar a esta performance a package CREAM usa uma mistura de algoritmos standard de álgebra universal juntamente com ferramentas de procura eficiente por modelos finitos de fórmulas de primeira ordem e a implementação de partes de código em C. Em geral, calcular congruências de álgebras é uma tarefa difícil. Existem vários teoremas descritivos para diferentes tipos de álgebra e algumas ferramentas computacionais para calcular congruências para álgebras finitas, mas geralmente essas ferramentas são aplicáveis a um conjunto muito específico e estreito de álgebras. O nosso objetivo era fornecer uma ferramenta eficaz para calculá-los para álgebras finitas do tipo (2m, 1 n ) abrangendo um conjunto muito amplo de álgebras, incluindo a maioria dos tipos e classes de álgebra atualmente estudados. O algoritmo usado foi o algoritmo de Freese cuja eficiência depende em muito da representação das álgebras e congruências. Em especial a representação de partições/congruências como um array é determinante na eficiência do cálculo das congruências principais uma vez que permite uma junção de blocos muito rápida, uma das operações mais utilizadas durante a execução do algoritmo de congruências. Além disso a representação usada não limita o âmbito geral das álgebras suportadas. No âmbito deste doutoramento vários algoritmos para o cálculo de automorfismos foram testados e a conclusão foi que o algoritmo mais promissor foi um algoritmo que usa invariantes das operações das álgebras para limitar os possíveis automorfismos da álgebra. Este algoritmo é usado na package Loops cuja implementação foi usada como guia tendo o seu âmbito sido expandido para suportar não só magmas mas qualquer álgebra do tipo (2 m, 1 n ). A implementação final dos algoritmos de automorfismos usando a abordagem de invariantes foi contribuída para a package CREAM por Choiwah Chow com base nas conclusões e no trabalho realizado no âmbito deste doutoramento. Dada a falta de referências sobre algoritmos para calcular endomorfismos, o algoritmo para calcular endomorfismos usado na package CREAM foi definido usando teoremas básicos de álgebra universal como o teorema do homomorfismo, para relacionar congruências, álgebras quocientes, subálgebras e endomorfismos. O algoritmo foi desenvolvido usando os algoritmos de congruências e automorfismos implementados, e uma aplicação denominada MACE4. O MACE4 [27] é uma aplicação de linha de comando que procura modelos finitos de fórmulas de primeira ordem. Embora o GAP seja adequado para prototipagem e implementação rápida de algoritmos, o código resultante não é muito rápido devido ao facto de ser uma linguagem interpretada. Reescrever o código em C permitiu melhorias surpreendentes que alcançaram uma melhoria de até 670 vezes do código GAP para o código C. Além disso, a integração com o MACE4 permite combinar a eficiência de algoritmos como [15], com um amplo conjunto de possibilidades fornecidas por uma ferramenta eficiente na procura por modelos finitos de fórmulas de primeira ordem, dando uma flexibilidade muito grande à package CREAM. A package CREAM é em média 20 vezes mais rápida no cálculo de congruências dos tipos de semigrupos muito limitados que são suportados pela função CongruencesOfSemigroups da package Semigroups que é a função mais abrangente em GAP para o cálculo de congruências. A única aplicação que possui um âmbito semelhante em termos de álgebras suportadas é a interface de linha de comando UACalc, mas faz isso em jython, sem beneficiar do ecossistema existente na plataforma GAP. Quando comparado com o UACalc, o package CREAM é consistentemente mais de 3 vezes mais rápido. Relativamente a automorfismos e endomorfismos, a comparação com outras bibliotecas/aplicativos é muito difícil, uma vez que o suporte é limitado principalmente a grupos e outras estruturas algébricas intimamente relacionadas com grupos. Para essas álgebras, o desempenho das packages GAP Loops e Sonata são comparáveis e às vezes melhores do que a package CREAM. Essas bibliotecas por vezes contam com o uso de teoremas específicos para essas álgebras. Mas apenas a package CREAM suporta a maioria das álgebras estudadas em álgebra convencional e moderna. Dada a importância das congruências, automorfismos e endomorfismos para o estudo de estruturas algébricas, espera-se que a package CREAM com seu desempenho e versatilidade possa ser uma ferramenta útil para a comunidade GAP e um amplo grupo de matemáticos. O código resultante está disponível como o pacote GAP CREAM que está totalmente documentado.
- Finite bases for semigroup varietiesPublication . Pereira, Manuel Jorge Raminhos; Araújo, João; Lee, Edmond W. H.O objetivo deste trabalho é fornecer um atlas das bases de identidades para as variedades geradas por semigrupos e grupos de ordem pequena. Com o propósito de auxiliar os matemáticos que trabalham neste campo a encontrar informações com facilidade, foi implementado um website que executa em segundo plano um conjunto de algoritmos desenvolvidos no âmbito deste trabalho e ainda ferramentas de demonstração automática e construtores de modelos finitos, para que o utilizador tenha um guia automático e inteligente. Por exemplo, o site fornece a primeira lista completa de variedades geradas por semigrupos de ordens iguais ou inferiores a 5, e consegue identificar rapidamente se a variedade gerada por um semigrupo inserido pelo utilizador, mesmo para ordens bastante superiores, coincide com uma das 218 variedades presentes na base de dados (atualmente inclui ainda outras 11 variedades geradas por semigrupos de ordens superiores). O site também fornece bases de identidades para classes arbitrariamente grandes de semigrupos, como bandas, ou a identificação dos semigrupos de ordem 6 conhecidos que geram variedades de base não finita. Além desta base de dados, o site propõe ainda uma lista das variedades geradas pelos semigrupos de ordem 6, num total de 414 conjeturas para novas variedades, entre as 463 identificadas neste trabalho e retirando as 49 variedades já conhecidas. O site disponibiliza ainda a informação para variedades geradas pelos grupos de ordens iguais ou inferiores a 255, obtida em resultado do levantamento e análise da literatura existente sobre as variedades geradas por estes grupos, para um total de 7012 grupos. O tratamento da informação recolhida para variedades geradas por grupos foi efetuado em GAP e através do desenvolvimento de algoritmos específicos para grupos comutativos e grupos metabelianos, nomeadamente para obtenção das identidades especificas de cada grupo, quando possível. O site oferece ainda um conjunto de funções sobre semigrupos, como encontrar o mínimo lexicográfico das cópias isomórficas de um dado semigrupo. Em relação à propriedade de base inerentemente não finita, o site pode decidir se um determinado semigrupo finito possui ou não essa propriedade; calcular a decomposição do semigrupo em semireticulados; ou converter a sintaxe da tabela de multiplicação de um semigrupo para utilização no GAP ou num demonstrador automático de teoremas/construtor de modelos finitos. O site fornece algumas outras funcionalidades, como uma ferramenta que gera a tabela de multiplicação de um semigrupo fornecida por uma apresentação em C, onde C ´e qualquer classe de álgebras definida por um conjunto de fórmulas em predicados de primeira ordem. A operação no sentido inverso também está acessível. O site disponibiliza um conjunto de informações e funcionalidades sobre variedades e as suas bases de identidades, como apresentar todas as inclusões entre as variedades da base de dados (variedades que são sub-variedades de outras variedades, que as contem) em formato gráfico, identificar se a variedade gerada por um semigrupo coincide com uma existente na base de dados, ou identificar a variedade cuja base é equivalente ao conjunto de identidades inseridas pelo utilizador. O site consegue ainda listar todas as variedades da base dados cujas bases de identidades implicam ou são implicadas por um conjunto de identidades definidas pelo utilizador. Neste cálculo o site leva em conta o conhecimento prévio de todas as inclusões entre variedades acima referidas para acelerar o cálculo e minimizar o uso do demonstrador automático de teoremas/construtor de modelos finitos. No desenvolvimento deste site foram utilizados: na implementação de algoritmos no servidor, Python, substituído pela versão compilada Cython em todos os cálculos intensivos; no desenvolvimento da interface cliente, JavaScript, JQuery, Ajax, Flask, HTML5, CSS3, Bootstrap e MathJax; em bases de dados relacionais, MySQL e SQLAlchemy; na preparação da informação presente nas bases de dados: GAP-System e em particular os “packages” smallsemi e smallgroups; na demonstração automática de teoremas e construção de modelos finitos, Prover9 e Mace4; na apresentação de diagramas, Graphviz. Foi desenvolvido um extenso conjunto de algoritmos reutilizáveis, para manipulação de variedades, semigrupos e grupos, organizados em bibliotecas, destacando-se: varlib.pyx – Implementa os algoritmos de cálculo intensivo do site, como o algoritmo que encontra o mínimo lexicográfico das cópias isomorfas de um dado semigrupo, ou o que verifica se um dado semigrupo satisfaz a base de identidades de uma das variedades na base de dados, e não satisfaz as identidades que definem as sub-variedades maximais. Por questões de velocidade, não existe nesta biblioteca recurso a demonstradores automáticos de teoremas ou a construtores de modelos finitos, sendo a sua funcionalidade substituída por algoritmos desenvolvidos otimizados para identidades, correndo nesta biblioteca a uma velocidade tipicamente 1000x superior ao mesmo programa em Python interpretado; p9m4tools.py – Implementa os algoritmos que recorrem ao demonstrador automático de teoremas e construtor de modelos finitos, embora em ´ultimo recurso, por questões de desempenho, através da implementação de diversas técnicas de “cache”. Nesta biblioteca estão por exemplo os algoritmos desenvolvidos para obter um semigrupo e a sua tabela de multiplicação a partir de uma apresentação, e filtrar as variedades cuja bases de identidades implicam, são implicadas por, ou são equivalentes a um conjunto de identidades entradas pelo utilizador; vartools.py – Implementa rotinas de menor exigência computacional, como a interpretação da entrada de dados do utilizador (por exemplo tabelas de multiplicação em diversos formatos à escolha do utilizador) e a formatação dos dados a apresentar, quer em texto que de forma gráfica. Esta biblioteca inclui ainda diversos algoritmos sobre semigrupos, como a decomposição em semireticulados. Este trabalho também contribui para a extensão da base de dados de variedades conhecidas: existem 28634 semigrupos de ordem 6, considerados equivalentes quando isomorfos ou anti-isomorfos. As variedades de 2035 desses semigrupos não coincidem com nenhuma variedade conhecida gerada por semigrupos de ordem até 5. Neste projeto, com base no teorema de Birkhoff e aplicando novos algoritmos de computador e uma ferramenta de demonstração automática de teoremas/construtor de modelo finitos, foi possível dividir esses 2035 semigrupos em 463 conjuntos de semigrupos que satisfazem as mesmas identidades, correspondendo a 414 novas variedades propostas (dado que são já conhecidas 45 variedades de base finita e 4 variedades de base não finita, geradas por semigrupos da ordem 6). Além disso, as identidades candidatas para a bases de identidades para todas estas novas variedades também são propostas e apresentadas nesta tese, acompanhadas por todas as tabelas de Cayley e os IDs no “package” GAPs smallsemi correspondentes, para cada conjunto de semigrupos encontrados que geram a mesma variedade conjeturada. As provas dessas novas variedades representam problemas em aberto e um desafio para todos os matemáticos nesta área. A mesma metodologia pode ser utilizada para encontrar novas variedades candidatas geradas por semigrupos de ordem 7 ou maior (no âmbito deste trabalho foram encontrados 73807 semigrupos não isomorfos de ordem 7 cujas variedades não coincidem com as variedades registadas na base de dados do site). Esta tese começa com um artigo 1 de pesquisa sobre variedades de semigrupos que contém a maior parte do conteúdo matemático desta tese. Este trabalho representa diversas contribuições para o campo do estudo das variedades de semigrupos: pela primeira vez foi reunida a informação dispersa sobre todas as variedades geradas por semigrupos de ordem igual ou inferior a 5, e relativa aos grupos de ordem igual ou inferior a 255, sendo apresentada num site de fácil utilização. O site oferece ainda um conjunto de funcionalidades sobre semigrupos e sobre variedades da base de dados, alicerçadas num conjunto de algoritmos desenvolvidos para maximização da performance e integrando uma interface, transparente para o utilizador, com um demonstrador automático de teorema e um construtor de modelos finitos, funcionando em paralelo para resultados mais rápidos. Adicionalmente, este trabalho contribuiu para o enriquecimento da base de dados de variedades geradas por semigrupos, ao propor conjeturas para todas as variedades não conhecidas geradas por semigrupos de ordem 6 e respetivas bases de identidades. As principais limitações deste trabalho estão relacionadas com o fato de alguns dos algoritmos desenvolvidos exigirem uma utilização intensiva de recursos computacionais (memória e processador). Estes algoritmos, ou não são adequados para colocação no site (como a pesquisa de novas variedades e respetivas bases), ou exigem limitações dos parâmetros de entrada (por exemplo o cálculo do mínimo lexicográfico, a geração de semigrupos a partir de apresentações, e a identificação de variedades, estão limitados a semigrupos de ordem inferior ou igual a, respetivamente, 10, 20 e 100). Noutras situações, embora raras, o site pode atingir o limite de memória permitido a cada utilizador. Este trabalho inspirou um alargado conjunto de ideias para trabalho futuro, e a primeira consiste na criação de um “package” GAP. Além de oferecer tudo o que site oferece e sem as limitações de memória e processador do site, o utilizador pode realizar múltiplas operações de forma automática. Na realidade o grosso do trabalho está pronto, já que este “package” se pode materializar apenas com o desenvolvimento de uma pequena camada de interface de comandos GAP, já que todos os algoritmos do site estão em bibliotecas autónomas e prontos para ser invocados por qualquer programa externo (aliás o acesso pelo GAP a rotinas das bibliotecas do site foi testado com sucesso no âmbito deste trabalho). Outras ideias para trabalho futuro passam por estender a procura de variedades `as variedades geradas por semigrupos de ordem 7; melhorar os algoritmos atuais para propor também as identidades que definem as sub-variedades maximais; automatizar a demonstração das variedades conjeturadas; desenvolver uma interface no site que permita a extensão da base de dados com novas variedades pelos matemáticos; aumentar as funcionalidades sobre variedades de grupos; desenvolver novo algoritmo para acelerar o cálculo do mínimo lexicográfico.
- ProverX: rewriting and extending prover9Publication . Robert, Ivo; Araújo, João; Veroff, RobertO propósito principal deste projecto é tornar o demonstrador automático de teoremas Prover9 programável e, por conseguinte, extensível. Este propósito foi conseguido acrescentando um interpretador de Python, uma linha de comandos e uma biblioteca de módulos, objectos e funções escritos em Python para interagir com ficheiros de Prover9 e Mace4. Foi também criada uma “interface” gráfica de utilizador (GUI) sob a forma de uma aplicação web para trazer aos utilizadores um meio mais eficiente e rápido de trabalhar com demonstrações automáticas de teoremas. A nova biblioteca de “scripting” oferece aos utilizadores novas funcionalidades tais como correr várias sessões simultâneas de Prover9 parando automaticamente quando uma demonstração (ou um contraexemplo) é encontrada, elaborar estratégias para aumentar a velocidade com que as demonstrações são encontradas ou diminuir o tamanho das mesmas. Outro módulo permite interagir com o sistema de álgebra GAP. Sobre esta biblioteca, muitas outras funcionalidades podem ser facilmente acrescentadas pois o objectivo principal é dar aos utilizadores a capacidade de acrescentar novas funcionalidades ao Prover9. Resumindo, o objectivo deste projecto é oferecer à comunidade matemática um ambiente integrado para trabalhar com demonstração automática de teoremas.
- Computing the intersection of two quadrics through projection and liftingPublication . Trocado, Alexandre Emanuel Batista da Silva; Gonzalez-Vega, Laureano; Araújo, JoãoO objetivo desta dissertação é o estudo da interseção de duas quádricas, do ponto de vista teórico através da demonstração de novos resultados e, do ponto de vista prático, implementando um algoritmo em dois softwares, o GeoGebra e o Maple. As quádricas são as mais simples superfícies curvas e determinar a sua interseção tem sido um problema de interessante resolução nas últimas décadas. Com o aumento do uso de computadores, a sua determinação e descrição ganhou uma maior relevância. Muitos problemas surgem frequentemente em aplicações de engenharia, modelação geométrica, projeto assistido por computador e robótica [2]. Um grande número de algoritmos foi proposto em [6], [23] e [2], baseados em técnicas aritméticas de ponto flutuante sensíveis a erros de arredondamento e com baixos tempos de execução em detrimento da precisão. Por outro lado, métodos simbólicos baseados na aritmética exata garantem a exatidão dos resultados, mas com tempos de execução altos. Portanto, a técnica a ser usada ao lidar com problemas de interseção deve ser cuidadosamente escolhida para obter tempos de execução aceitáveis. Durante vários anos deve-se a Levin ([27] e [28]) o único método geral conhecido para a determinação e representação da interseção de duas quádricas. Este método basea-se na análise do conjunto definido pela combinação linear das duas quádricas. No entanto, este método, por vezes, falha quando a curva de interseção é singular ou quando é usado um método de representação que recorre a ponto flutuante. Ao longo do tempo, este método proposto por Levin foi alvo de diferentes melhorias e recentemente Dupont e outros ([12], [13], [14]) propuseram um algoritmo que determina, recorrendo à análise de várias dezenas de casos no espaço projetivo, a interseção de duas quádricas. A performance deste algoritmo foi analisada em [26]. Nesta dissertação, o método utilizado recorre à projeção num plano da curva de interseção, à análise da topologia dessa curva e ao seu levantamento. Este trabalho inclui três artigos, um submetido para publicação (ver Capítulo 2) e dois outros publicados (ver Capítulos 3 e 4). Porquê o recurso ao GeoGebra e ao Maple? O GeoGebra é um software de geometria dinâmica que pode ser usado em todos os níveis de ensino que combina funcionalidades de Geometria 2D, 3D, álgebra, cálculo algébrico simbólico (CAS), representação gráfica, cálculo e estatística. A este software está associada uma larga comunidade de utilizadores espalhada pelo mundo, fazendo com que este seja considerado um dos softwares mais utilizados na educação ao nível do ensino básico e secundário. Por outro lado, o Maple é um poderosa ferramenta de cálculo algébrico simbólico. Esta ferramenta permite que estudantes, educadores e matemáticos consigam efetuar cálculo simbólico, numérico e construção de algoritmos, programáveis através de uma linguagem e comandos próprios, combinando assim, o poder dos algoritmos com as funcionalidades do CAS. De uma forma geral, o GeoGebra tem a vantagem de ser um software livre, de código aberto e de utilização simples que permite a interação com os objetos matemáticos, em diferentes perspetivas, de uma forma bastante intuitiva. No entanto, algumas das suas funcionalidades ainda possuem algumas limitações, em particular, a interseção de objetos 3D. Por outro lado, o Maple tem a desvantagem de ser um software comercial, por dificultar a utilização universal, e a interação com os objetos matemáticos não é tão intuitiva como o do GeoGebra, mas os seus packages permitem lidar com conteúdos matemáticos muito mais exigentes do que o GeoGebra. O primeiro artigo é dedicado à descrição do método, definindo uma estrutura teórica também usada nos dois artigos seguintes. Neste primeiro artigo, novos resultados são apresentados: a forma para determinar a expressão analítica da curva de projeção (cutcurve) que deve ser definida numa região plana delimitada pelas curvas silhueta (curvas de projeção dos limites de ambas quadricas); um método para determinar pontos singulares da curva de projeção e pontos comuns entre a cutcurve e as curvas de silhueta. O método algébrico foi definido recorrendo a resultantes e subresultantes, sendo o seu desempenho testado através de uma implementação no software Maple. Em alguns casos, foi possível determinar a exata parametrização da curva de interseção (envolvendo radicais se necessário), noutros o resultado (topologicamente correto) foi apresentado como o levantamento da discretização dos ramos da curva de projeção, uma vez que os seus pontos singulares estejam todos determinados. O principal objetivo do segundo artigo é criar uma ferramenta para determinar a curva de interseção de duas quadráticas. Algo que o GeoGebra permite apenas para casos muito simples. Neste artigo, é apresentada uma implementação do algoritmo descrito no primeiro artigo, no GeoGebra. Essa implementação é feita usando apenas comandos do GeoGebra que interagem com as janelas Álgebra, CAS, 2D e 3D. Para testar a eficiência e aplicabilidade desse algoritmo (e a sua implementação no GeoGebra), foram gerados aleatoriamente e testados 50 exemplos. Os casos analisados foram aqueles em que duas quadráticas são definidas por dois polinómios de grau 2, na variável z, o caso de uma quádrica é definida a partir de polinómio de grau 2 e de um polinómio de grau 1 e, finalmente, o caso em que as duas quadráticas são definidas por dois polinómios do grau 1 na variável z. No terceiro artigo, é apresentada a implementação no software Maple do método descrito e analisado no primeiro artigo. O comando intersectplot do Maple representa a curva de interseção, num espaço tridimensional, entre duas de superfícies bidimensionais. Neste artigo, mostra-se como essa implementação no Maple melhora os resultados produzidos pelo comando intersectplot quando se determina a curva de interseção entre duas quádricas em 3D. Esta abordagem não pretende classificar a curva de interseção entre as duas quadráticas consideradas. O principal objetivo é produzir de maneira muito direta uma descrição da curva de interseção que seja topologicamente correta. Esta é a razão pela qual permitimos que o levantamento da curva de projeção, quando possível, recorra ao uso de radicais ou contamos com a discretização dos ramos da curva de projeção (determinados exclusivamente pelos pontos determinados nessa curva). A implementação no GeoGebra mostrou-se funcional, mas demonstrou ser lenta nos casos em que exitiram muitos pontos singulares da curva da curva de projeção. Usando esse processo, pontos singulares que vêm da interseção tangencial não foram determinados e esses pontos podem ser produzidos pela função locus GeoGebra. Alguns problemas técnicos foram detectados pela falta de precisão do comando do locus do GeoGebra durante a representação da curva de projeção, o que não invalidou o funcionamento correto do algoritmo. Em alguns casos, o GeoGebra poderá produzir melhores resultados se for possível aumentar a precisão da funcionalidade locus. Em relação à implementação do algoritmo no Maple, seu desempenho foi analisado apenas nos casos mais complicados, nos quais as duas quadráticas são definidas por polinómios de segundo grau em z. Em alguns desses casos, foi possível obter a parametrização exata da curva de interseção mesmo com radicais. É possível destacar que alguns pontos não determinados pelo comando intersectplot do Maple foram calculados, usando o método descrito nesta dissertação. Num futuro próximo, o desempenho do algoritmo poderá ser otimizado e a sua implementação no Maple deverá considerar não apenas o caso geral, ou seja, considerar as duas quadrádicas definidas por polinómios de grau menor que 2 na variável z.
- Conjugation in abstract semigroupsPublication . Borralho, Maria de Fátima Lopes; Araújo, João; Kinyon, Michael K.On a semigroup S with a xed element c, we can de ne a new binary operation x c y := xcy for all x; y 2 S. Then (S; c) is a semigroup called the variant of S at c. Elements a; b 2 S are said to be primarily conjugate or just p-conjugate, if there exist x; y 2 S1 such that a = xy; b = yx. In groups this coincides with the usual conjugation, but in semigroups, it is not transitive in general. Finding classes of semigroups in which primary conjugacy is transitive is an interesting open problem. Kudryavtseva proved that transitivity holds for completely regular semigroups, and more recently Araújo et al. proved that transitivity also holds in the variants of completely regular semigroups. They did this by introducing a variety W of epigroups containing all completely regular semigroups and their variants, and proved that primary conjugacy is transitive in W. They posed the following problem: is primary conjugacy transitive in the variants of semigroups in W? In this thesis, we answer this a rmatively as part of a more general study of varieties of epigroups and their variants, and we show that for semigroups satisfying ∈ xy {yx, (xy)n} for some n > 1, primary conjugacy is also transitive.