| layout | title | subtitle |
|---|---|---|
page |
Links |
- UITP (User Interfaces for Theorem Provers) workshop series.
- MathUI (Mathematical User Interfaces) worshop series.
- ITP (Interactive Theorem Proving) conference series (evolution/merger of TPHOLs and others).
- MKM (Mathematical Knowledge Management)
- 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.