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 Seiten 65-80 Lecture Notes in Artificial Intelligence 3863 ISBN 978-3-540-31430-1 Springer Berlin, Heidelberg 2005.

Abstrakt

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.

mkm05.pdf (pdf, 475 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence