Browsing by Issue Date, starting with "2020-01-22"
Now showing 1 - 1 of 1
Results Per Page
Sort Options
- 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.