Proof General: A Generic Tool for Proof Development

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication6th International Conference, TACAS 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000 Berlin, Germany, March 25 – April 2, 2000 Proceedings
EditorsSusanne Graf, Michael Schwartzbach
PublisherSpringer Berlin Heidelberg
Pages38-43
Number of pages6
Volume1785
ISBN (Electronic)978-3-540-46419-8
ISBN (Print)978-3-540-67282-1
DOIs
Publication statusPublished - 2000

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume1785

Fingerprint Dive into the research topics of 'Proof General: A Generic Tool for Proof Development'. Together they form a unique fingerprint.

Cite this