2026-09-25T13:53:36Zhttps://repositorioaberto.uab.pt/server/oai/requestoai:repositorioaberto.uab.pt:10400.2/99252025-05-26T11:44:52Zcom_10400.2_15583com_10400.2_15395com_10400.2_15392col_10400.2_15585
Araújo, João
Veroff, Robert
Robert, Ivo
2020-08-05T14:25:04Z
2020-08-05T14:25:04Z
2020-01-22
2020-08-05
Robert, Ivo - ProverX [Em linha]: rewriting and extending prover9. [S.l.]: [s.n.], 2020. 144 p.
http://hdl.handle.net/10400.2/9925
urn:tid:101614918
101614918
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.
The primary purpose of this project is to extend Prover9 with a scripting language.
This was achieved by adding a Python interpreter, an interactive command line and a special
scripting library to interact with Prover9 and Mace4 files. A user interface in the form of a web
application was also created to help users achieve a more rapid and efficient way of working with
automated theorem proving.
The new scripting library offers utilities that allows a user to run several Prover9 sessions
concurrently and to create strategies for increasing the effectiveness of the proof search or to search
for shorter proofs. Another module allows to interact with the algebra system GAP.
Based on the library, many more functionalities can be easily added, as the main goal is to give users
the ability to extend the functionality of Prover9 the way they see fit.
In conclusion, the aim of this project is to offer to the mathematical community an integrated
environment for working with automated reasoning
eng
Prover9
Mace4
Demonstração automática de teoremas
Python
GAP
Automated theorem proving
ProverX: rewriting and extending prover9
doctoral thesis
Tese de Doutoramento em Álgebra Computacional em associação com a Faculdade de Ciências e Tecnologia da Universidade de Coimbra, apresentada à Universidade Aberta
0000-0001-8473-2089
Publication
04:Educação de Qualidade
openAccess
doctoralThesisopen.access