Proof General - Assisted Proof Document Authoring

We present an authoring system for formal proof which addresses the concerns of efficiently producing formal proof developments together with human-readable documentation. To start, we consider a central document format which, in the tradition of literate programming, allows one to extract either a formal proof script or a human-readable rendering; the two may have differing structure and detail levels, but are developed together in a synchronised way. On top of this, we introduce ways for assisting the production of the central document, by allowing tools to contribute backflow to update and extend the document automatically. Our authoring system extends the new PG Kit architecture for Proof General, which brings the extra advantage that it fits into a uniform interface that is generic across different theorem proving systems.
David Aspinall, Christoph Lüth and Burkhart Wolff.
Assisted Proof Document Authoring
Mathematical Knowledge Management 2005 (MKM '05), Springer LNAI 3863, p. 65--80, 2005.
Download as pdf.


Click here to return to my papers page.

my Vcard
David R. Aspinall, email david.aspinall@ed.ac.uk.
Contact GPG key (Instant HOWTO)