Current version is 0.89.170316

PhoX is a

- Version 0.89: adapted to recent OCaml 4.XX. Remark: not yet adapted to recent ProofGeneral Emacs mode.
- Version 0.85: more bugs fixed, lots of improvement, first experimental version of proof by contextual menu (needs a very recent cvs version of Proof General.
- Version 0.83: more bugs fixed and started to clean the software for more natural names and behavior for commands.
- Version 0.82: more bugs fixed and most of the tutorials translated to english.
- New version (version 0.8): better tutorials and documentation.
- Version 0.8 tested successfully under MAC OS X (thanks to Laurent Chéno).
- Coming later (version 0.9): a much more powerful module system.

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!):

- Proofs are developed in a natural deduction style, but the left rules and cut rule of sequent calculus are also available (offering a maximum freedom).
- Automatic theorem proving is provided to help you finish the
*easy*cases. This is quite useful but there are still a little place for improvement here (coming soon). - Equational reasoning is provided in two forms: rewriting (you can rewrite
a
*goal*or an hypothesis using one or more equations) and automatic (when 2 or 3 equations are needed, and sometimes more, an automatic equational reasoning algorithm can discover for you that two expressions are equal). Moreover, conditional equations are supported (the conditions necessary to apply a given equation may be proven automatically or left to you). - The rules (sometimes called tactics) can be extended by the user. After defining a predicate, you can prove some new theorems and add them as introduction or elimination rules. You can also control the way the automatic reasoning uses your new rules.
- After finishing a proof, a proof tree is constructed and checked (by a small piece of code). This means that the correctness of your proof is independent from the correctness of the tactics you used (including the automatic reasoning).
- A module system is provided. For instance, you can prove results about groups using the usual axioms on groups and then reuse your results on other groups. In future version, the module system will allow quantifications on modules ...
- The syntax is extensible. This makes your PhoX source files more readable.
- The program can assist you to extract a LaTeX article from your formalization.
Formulas from the current context during a proof can be translated into
a LaTeX version. You can customized the way these formulas are produced.
This means that you can write
*normal*articles because the text is not automatically generated ! - We recommend you use Proof General as an interface using the Xemacs editor. You can have a look at a screen shot.

- You can browse the reference manual and the user's manual of the library .
- Otherwise, you may downlad a ps or dvi version of the presious manuals, see the distribution section
- Computer Assisted Teaching in Mathematics is an article describing a teaching experiment using PhoX. This paper constitutes a very good introduction to PhoX, with one detailed example and a short index of the main commands. It is also available in french
- The distribution comes with various kinds of tutorials (in french only). Some of them are intended to learn PhoX, others are intended to learn Mathematics.
- For bug report, send me
a mail at the address
`Christophe.Raffalli@univ-savoie.fr`with a precise description of the problem.

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

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.

- github repository
- opam package
- You will need Objective Caml (version 4.02 or more)
- You can also download the manuals:
- Reference manual (ps format)
- Reference manual (dvi format)
- Users manual of the library (ps format)
- Users manual of the library (dvi format)
- PhoX's cvs tree

Christophe Raffalli /LAMA, Savoie University / raffalli@univ-savoie.fr Last modified: Tue Mar 1 17:30:58 CET 2005