ProofWeb is a web-based interface
to interactive theorem provers run on a server. It is being enhanced
towards a Wiki for formalized mathematics.
I3P is an
IDE-based interface for Isabelle using Proof
General-style interaction. It’s perhaps in a more robust state than
our own Proof General Eclipse prototype.
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.
Prosper was 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.
Isamode was an XEmacs
front-end for Isabelle. It had a different feature collection
compared with Proof General: script management wasn’t supported, but
menus and shortcuts provided one of the first widely used enhanced
interfaces for Isabelle.
CtCoq was an
interface for the Coq theorem prover, developed at INRIA, Sophia
Antipolis, as part of Projet
CROAP. Like Proof General, CtCoq
used a general approach for building user-interfaces for
theorem provers. 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.