PhoX

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 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 para grandes generaciones

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

Control de autoridades|

* Proyectos Wikimedia
* Datos: Q603143

|

* Datos: Q603143