Guillaume BUREL's Homepage (Guillaume Burel's photo)

Tools

I developed the following software:

iProver Modulo
The integration of polarized resolution modulo into the automated theorem prover iProver.
CoqInE
A translator of Coq proofs into Dedukti, a universal proof checker based on the lambda-Pi-calculus modulo formalism.
autotheo
A tool that takes the axioms from a TPTP file and that transforms them into a rewriting system usable by iProver modulo.