Organize your proofs!
 Home |
Features |
Download |
Documentation |
About |
| News |
Screenshots |
Development |
Publications |
Related |
|
|
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 manager and main developer 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
Makarius.
|
 |
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.
|
There are also unsupported or experimental instances of Proof General, including
These instances may be incomplete or not work with the latest theorem prover versions.
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. We welcome offers to support, extend and improve Proof General instances. Please get in touch if you plan major work.
If you are considering supporting (or implementing) a new prover, please read about the Proof General Kit architecture. The idea is that proof assistants should support PGIP, a uniform protocol for interaction, rather than use system-specific customization inside interfaces. The main research prototype using PGIP is an experimental Eclipse plugin, although Emacs Proof General supports some PGIP configuration.