Álgebra Computacional | Computational Algebra
Permanent URI for this community
Browse
Browsing Álgebra Computacional | Computational Algebra by Subject "Automated theorem proving"
Now showing 1 - 3 of 3
Results Per Page
Sort Options
- 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?
- Forbidden substructure theoremsPublication . Ferreira, Fernando Manuel Maia; Araújo, João; Kinyon, Michael
- 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.