A nice picture, too bad!

The PhoX Proof Assistant

Current version is 0.90.270624 (June 2024)

New: PhoX online is available
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 stable and not planned to evolve. This means that PhoX any file should work in the future. PhoX is used for some exercise of our book "Introduction à la logique".

Contents

  • An overview
  • Documentation
  • Examples
  • The team
  • The distribution

  • 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

    Christophe Raffalli
    christophe@raffalli.eu
    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.
    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, before we used proof general.

    PhoX distribution and documentation (0.90)


    Changes


    Christophe Raffalli