Proof General: A Generic Tool for Proof Development

12 years 7 months ago
Proof General: A Generic Tool for Proof Development
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 proofgen. 1 Background Proof General is a generic interface for interactive proof assistants. A proof assistant is a computerized helper for developing machine proofs. There are many uses for machine ...
David Aspinall
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 2000
Authors David Aspinall
Comments (0)