A nice picture, too bad!

The PhoX Proof Assistant

Beware: work in progress.

Current version is 0.88.100524.


PhoX is a proof assistant based on High Order logic and it is eXtensible. One of the principle of this proof assistant is to be as user friendly as possible and so to need a minimal learning time. The current version is still expirimental but starts to be really usable. It is a good idea to try it and make comments to improve the final version.

Hot news


Contents

  • An overview
  • Documentation
  • Examples
  • The team
  • The distribution
  • Exercises for math students formalized on computers (not only with Phox)

  • PhoX overview

    The major design goal of this program was to make as easy as possible the formalization of mathematical proofs on machine. This is quite a hard goal to reach. For instance, if you consider knots theory, you will have great problems to translate your graphical proofs !

    However, I have put a lot of work to make it possible to formalize a lot of mathematics quite easily. Here are a list of the features offered by this program (quite a few of them are unique!):


    Documentation


    Examples

    Here is a very simple proof development: a proof of the existence of the quotient and remaining of the euclidain division. You can browse


    The team

    All people working on PhoX are member of the Laboratory of Mathematic of the Savoy University or the Logic Team of Paris VII university. Although some part of the code where written while C. Raffalli was at L.F.C.S. in Edinburgh or at Chalmers university.

    Christophe Raffalli
    Christophe.Raffalli@univ-savoie.fr
    Author of most of the implementation.
    Philippe Curmin
    curmin@logique.jussieu.fr
    P. Curmin is working on a marking algorithm to optimise extracted programs. This work should be useful in future versions.
    Pascal Manoury
    eleph@logique.jussieu.fr
    P. Manoury may port in the future the ProPre system within PhoX. This should allow a lot of totality proofs to be automatized (proof that a given equational definition of a function always terminates)
    Paul Roziere
    roziere@logique.jussieu.fr
    P. Roziere formalized quite a few proofs in the system and is responsible for most of the emacs mode.

    PhoX distribution (0.85)


    Christophe Raffalli /LAMA, Savoie University / raffalli@univ-savoie.fr
    Last modified: Mon May 24 10:34:14 CEST 2010