ProverX: Rewriting and Extending Prover9

Abstract

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.

Alternate abstract:

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.