PhoX

En la Demostració automàtica de teoremes, PhoX és un asistenete de proves que és extensible. L'usuari li dona a PhoX un objectiu inicial, guiant-li a través dels subobjetivos i proves, per a aplegar a l'objectiu final. Internament, PhoX construïx arbres de deducció naturals. Cada fòrmula provada en anterioritat pot convertir-se en una regla futura per a grans generacions

PhoX va anar originalment dissenyat i implementat per Christophe Raffalli en el llenguage de programació OCaml. Ell ha continuant guiant el desenroll actual, frut d'una colaboració entre l'Universitat de Savoy i l'Universitat Paris VII.