Carlos Sousa

Prover 9 input file Translator

Currently there are several theorem provers, but their proof finding performance is highly sensitive to the problem we are working on. 
Since now we can lunch different computer processes simultaneously, the right thing to do would be to ask the same question to several different provers. The main difficulty is that every prover has its own input format and the user must “waste” time writing the same problem in different  formats.
The aim of my work is to produce an automatic translator from Prover9 input files to other software prover applications format. The final goal is to turn automatic the process of lunching jobs in various theorem prover apps using only Prover9 input files. The first finding the answer kills all other processes.