Organize your proofs!  Home  Features  Download  Documentation  About  News  Screenshots  Development  Publications  Related

Related Workshops and Conferences

• 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)

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.