
The PhoX Proof Assistant

Current version is 0.89.170316
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
- 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.
- A Windows version is available. See its specific installation instructions.
- 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.
Contents
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!):
- 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.
Documentation
- 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.eu
with a precise
description of the problem.
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 were 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.89)
Christophe Raffalli Last modified: Tue Mar 1 17:30:58 CET 2005