Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Proof General: A Generic Tool for Proof Development
| |
|
Proof General: A Generic Tool for Proof Development
David Aspinall6 
| (6) |
LFCS, University of Edinburgh, UK |
Abstract
This note describes Proof General, a tool for developing machine proofs with an interactive proof assistant. Interaction is based around a proof script, which is the target of a proof development. Proof General provides a powerful user-interface with relatively little effort,
alleviating the need for a proof assistant to provide its own GUI, and providing a uniform appearance for diverse proof assistants.
Proof General has a growing user base and is currently used for several interactive proof systems, including Coq, LEGO, and
Isabelle. Support for others is on the way. Here we give a brief overview of what Proof General does and the philosophy behind
it; technical details are available elsewhere. The program and user documentation are available on the web at http://www.dcs.ed.ac.uk/home/proofgen.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|