INRIA Sophia Antipolis
CHOL distribution
What it is:
CHOL is an attempt to provide a better user-interface
for the
HOL theorem prover. It has been developed following
a general approach for building user-interfaces for theorem provers. Its characteristics are the following:
- graphic interface:
- Multi fonts and colors are used to display
formulas and commands.
- structured editing:
- The proof of a proposition is presented as the structured editing
of the tactic that proves the proposition.
- rewriting tool:
- A tool has been developed that filters the theorems of the database
with respect to the term to rewrite.
- separation between the interface and the prover:
- The X interface and HOL run as two separate processes.
How to get it:
The interface runs with the following versions of HOL: HOL88(AKCL) and HOL90 (SML/NJ). The compressed tarfile is 6 MBytes and the full interface takes
15 MBytes. For the moment, only the version for SUN4OS4 is
directly available by ftp. If you need other architectures,
please send me an email.
If you are interested in getting CHOL, click
here.
If you only want to have a look at the documentation, click here.
If you have an old version, a tarfile is available
to update the sml version for hol90.7
Problems and suggestions
I continue to maintain and develop the interface. So email
me any problems, bug reports, or suggestions.
Click here for a summary of the messages
so far.
CHOL profits from work done on programming environments, in particular
the
Centaur
system, developed in the
Croap group
at
INRIA Sophia Antipolis.
Laurent Théry / INRIA Sophia Antipolis/ Laurent.Thery@inria.fr