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 http://www.dcs.ed.ac.uk/home/ 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 ...

• Type: Conference
• Year: 2000
• Where: TACAS
• Authors: David Aspinall
• Keywords: Algorithms, Proof Assistant, Proof General, Proof Script, TACAS 2000