Here are some links to related things.
If you have any suggestions
for links to include here, or find broken links, please
.
- Isamode
is an XEmacs front-end for Isabelle. It has a different
feature collection compared with Proof General:
script management is not supported, but there are extensive
menus and shortcuts provided for common Isabelle
commands.
- CtCoq
is an interface for the Coq theorem prover, developed
at INRIA, Sophia Antipolis, as part of
Projet CROAP.
Like Proof General, CtCoq is based on a general approach for
building user-interfaces for theorem provers, although no other
current theorem provers are supported. Unlike Proof General, CtCoq
is based on a graphical environment with structure editing,
created with the Centaur
system.
-
OMEGA is
a collection of web-based distributed tools for supporting
theorem proving.
-
Prosper is a project
to develop an extensible, open proof tool architecture for
incorporating formal verification into industrial CAD/CASE tool
flows and design methodologies. The tools include novel
user-friendly interfaces.
-
As a possible foundation for generic proof environments,
OpenMath
is a standard representation form for mathematical objects, which
links in with the MathML
markup language.