
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
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.
- 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 and uses math symbols represented by unicode
characters. 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 ! This feature will likely be replaced by a generation
of web page.
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
- 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
- Version 0.90 (2024): adapted to OCaml 5.XX + web version.
- Version 0.89 (2017): adapted to 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 1.0 or probably never): a much more powerful module
system. The idea is to add a form of record with subtyping to have first
class module in the logique. This also requires quantification over sort in formulas.
Christophe Raffalli