Section: New Software and Platforms

Autotheo

Autotheo is a tool that transforms axiomatic theories into polarized rewriting systems, thus making them usable in iProver Modulo. It supports several strategies to orient the axioms, some of them being proved to be complete, in the sense that ordered polarized resolution modulo the resulting systems is refutationally complete, some others being merely heuristics. In practice, Autotheo takes a TPTP input file and produces an input file for iProver Modulo.

• Contact: Guillaume Burel

• URL: http://www.ensiie.fr/~guillaume.burel/blackandwhite_autotheo.html.en

In 2015, we extended Autotheo so that it prints a derivation of the transformation of the axioms into rewriting rules. This derivation is in TSTP format and includes the CNF conversions obtained from the prover E.