PhoX

De Wikipedia, la enciclopedia libre
Saltar a: navegación, búsqueda

En la Demostración automática de teoremas, PhoX es un asistenete de pruebas que es eXtensible. El usuario le da a PhoX un objetivo inicial, guiándole a través de de los subobjetivos y pruebas, para llegar al objetivo final. Internamente, PhoX construye árboles de deducción naturales. Cada fórmula probada con anterioridad puede convertirse en una regla futura.

PhoX fue originalmente diseñado e implementado por Christophe Raffalli en el lenguaje de programación Ocaml. El ha continuando guiando el desarrollo actual, fruto de una colaboración entre la Universidad de Savoy y la Universidad Paris VII.