Publikation
Assisted Proof Document Authoring
David Aspinall; Christoph Lüth; Burkhart Wolff
In: Michael Kohlhase (Hrsg.). 4th International Conference on Mathematical Knowledge Management (MKM 2005). International Conference on Mathematical Knowledge Management (MKM-2005), July 15-17, Bremen, Germany, Pages 65-80, Lecture Notes in Artificial Intelligence, Vol. 3863, ISBN 978-3-540-31430-1, Springer, Berlin, Heidelberg, 2005.
Zusammenfassung
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.