PhoX ( 1994 ) é um assistente de prova desenvolvido por Christophe Raffalli na Universidade de Savoie e anteriormente em Jussieu com a participação de Philippe Curmin , Pascal Manoury e Paul Roziere .
Seu nome deriva do fato de que uma raposa (em inglês raposa) pode comer um galo ( Galo é outro ajudante de prova). Também significa P assistente de telhado em H igher O rder logic e X tensible.
Ele foi escrito na linguagem OCaml , e pode ser usado na maioria dos sistemas de computador como o Linux , o Windows e Mac OS X .
Como o próprio nome sugere em inglês, PhoX é baseado na lógica de ordem superior e é extensível. Um dos princípios deste programa é ser o mais fácil de usar possível e exigir pouco tempo de aprendizagem, que é usado para ensinar os alunos de matemática.
Aqui estão as diferentes características do PhoX:
PML