Assisted Proof Document Authoring

David Aspinall, Christoph Lüth, Burkhart Wolff

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

Abstract

Recently, significant advances have been made in formalised mathematical texts for large, demanding proofs. But although such large developments are possible, they still take an inordinate amount of effort and time, and there is a significant gap between the resulting formalised machine-checkable proof scripts and the corresponding human-readable mathematical texts. We present an authoring system for formal proof which addresses these concerns. It is based on a central document format which, in the tradition of literate programming, allows one to extract either a formal proof script or a human-readable document; the two may have differing structure and detail levels, but are developed together in a synchronised way. Additionally, we introduce ways to assist production of the central document, by allowing tools to contribute backflow to update and extend it. Our authoring system builds on the new PG Kit architecture for Proof General, bringing the extra advantage that it works in a uniform interface, generically across various interactive theorem provers.
Original languageEnglish
Title of host publicationMathematical Knowledge Management
Subtitle of host publication4th International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised Selected Papers
EditorsMichael Kohlhase
PublisherSpringer Berlin Heidelberg
Pages65-80
Number of pages16
ISBN (Electronic)978-3-540-31431-8
ISBN (Print)978-3-540-31430-1
DOIs
Publication statusPublished - 2006

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume3863

Cite this