ProverX: rewriting and extending prover9

O 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.

Name thesis:degree_name

Tese de Doutoramento em Álgebra Computacional em associação com a Faculdade de Ciências e Tecnologia da Universidade de Coimbra, apresentada à Universidade Aberta

Year dc:date.issued

2020

Author dc:creator

• Robert, Ivo

Advisors dc:contributor.advisor

• Araújo, João
• Veroff, Robert

• Prover9
• Mace4
• Demonstração automática de teoremas
• Python
• GAP
• Automated theorem proving

Language dc:language.iso

eng

Identifier URI

urn:tid:101614918

OAI identifier oai:identifier

oai:repositorioaberto.uab.pt:10400.2/9925