Organize your proofs!
 Home |
Features |
Download |
Documentation |
| News |
Screenshots |
Development |
About |
|
|
Organize your proofs!
|
Proof General is a generic front-end for proof assistants (also known as interactive theorem provers), based on the customizable text editor Emacs.
Proof General has been developed at the LFCS in the University of Edinburgh with contributions from other sites. It is distributed under the conditions of the GNU General Public License. The main developer and manager of the Proof General project is David Aspinall. Other contributors are listed below and in the AUTHORS file.
Proof General comes ready-to-go for these proof assistants:
 |
Isabelle Proof General for
Isabelle
By
David Aspinall
and
Markus Wenzel.
|
 |
Coq Proof General for
Coq
By Healfdene Goguen, Patrick Loiseleur, David Aspinall, and
Pierre Courtieu.
|
 |
PhoX Proof General for
PhoX
By
Christophe Raffalli,
Paul Roziere and Jean-Roch Sotty.
|
 |
LEGO Proof General for
LEGO
By Thomas Kleymann, Dilip Sequeira,
David Aspinall
and
Paul Callaghan.
|
There are also several experimental or in-development instances of Proof General, including
Instances of Proof General marked "in development" are not complete, but are supported by the developers of proof systems. The other instances above are "technology demonstrations" of Proof General for other provers, but only show a bare fraction of what is possible. We are seeking volunteers to support and improve each of these (please send a note to da+pg-feedback@inf.ed.ac.uk if you're interested).
Proof General is ready to be customized to new proof assistants. It can be very easy to get basic support working. Full documentation on configuration is provided.
If you are considering supporting a new prover, please note that the new architecture for Proof General Kit expects that the proof assistant will support a uniform protocol for interactive proof (rather than adhoc customization in Emacs Lisp). Exciting developments are in progress for this new architecture, such as additional alternative front-ends, including an Eclipse plugin.