|
Organize your proofs!
|
Related Workshops and Conferences
Related Projects, Present and Past
-
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.
Web pages by
David Aspinall.
Please report issues
on PG trac.
Last modified 22 May 2013.