Yves Robert

Extending Prover9

This talk aims to show a prototype of an application that extends Prover9/Mace functionality by adding Python scripting.
These are the first results of an ongoing PhD thesis in Computational Algebra at Universidade Aberta.
The modular architecture will be introduced first, followed by a small demonstration of the application and how it can be easily extended with scripts.
A version running on a web server will also be demonstrated.