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. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Aspinall, D., Lüth, C., & Wolff, B. (2006). Assisted proof document authoring. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3863 LNAI, pp. 65–80). https://doi.org/10.1007/11618027_5
Mendeley helps you to discover research relevant for your work.