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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abrial, J.-R., Cansell, D.: Click’n’prove: Interactive proofs within set theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 1–24. Springer, Heidelberg (2003)
Aspinall, D., Lüth, C.: Commentary on PGIP (September 2003), Available from http://proofgeneral.inf.ed.ac.uk/kit/
Aspinall, D., Lüth, C.: Proof General meets IsaWin. In: Aspinall, D., Lüth, C. (eds.) User Interfaces for Theorem Provers UITP 2003. ENTCS, vol. 103(C) (2003)
Aspinall, D., Lüth, C.: Parsing, editing, proving: The PGIP display protocol. In: User Interfaces for Theorem Provers UITP 2005 (April 2005)
Autexier, S., Benzmüller, C., Fiedler, A., Horacek, H., Bao Vo, Q.: Assertion level proof representation with underspecification. In: Kamareddine, F. (ed.) Proc. MKM Symposium MKM 2003, Edinburgh (November 2003)
Avigad, J.: Notes on a formalization of the prime number theorem. Technical report, Carnegie Mellon (2004)
Bertot, Y., Kahn, G., Théry, L.: Proof by pointing. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 141–160. Springer, Heidelberg (1994)
Brucker, A.D., Rittinger, F., Wolff, B.: HOL-Z 2.0: A proof environment for Z-specifications. Journal of Universal Computer Science 9(2), 152–172 (2003)
de Bruijn, N.G.: A survey of project Automath. In: Hindley, J.R., Curry, H.B. (eds.) Essays in Combinatory Logic, Lambda Calculus and Formalism, pp. 589–606. Academic Press, London (1980)
Dixon, L., Fleuriot, J.: A proof-centric approach to mathematical assistants. Journal of Applied Logic: Special Issue on Mathematics Assistance Systems (2005) (to appear)
Gonthier, G.: A computer-checked proof of the four colour theorem. Technical report, Microsoft Research Cambridge (2004), http://research.microsoft.com/~gonthier/4colproof.pdf
Grundy, J.: Transformational hierarchical reasoning. Computer Journal 39, 291–302 (1996)
Hales, T.C.: The Flyspeck project page., http://www.math.pitt.edu/~thales/flyspeck/index.html
Kamareddine, F., Maarek, M., Wells, J.B.: Flexible encoding of mathematics on the computer. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 160–174. Springer, Heidelberg (2004)
Kamareddine, F., Nederpelt, R.: A refinement of deBruijn’s formal language of mathematics. Journal of Logic, Language and Information 13(3), 287–340 (2004)
Knuth, D.E.: Literate programming. The Computer Journal 27(2), 97–111 (1984)
Kohlhase, M.: Semantic markup for TeX/LaTeX. In: Informal Proc. Mathematical User Interfaces, Math UI 2004 (2004)
Lüth, C., Wolff, B.: Functional design and implementation of graphical user interfaces for theorem provers. Journal of Functional Programming 9(2), 167–189 (1999)
Lüth, C., Wolff, B.: TAS — a generic window inference system. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 405–422. Springer, Heidelberg (2000)
Mackenzie, D.: What in the name of Euclid is going on here? Science 307, 1402–1403 (2005)
Relax Ng Xml schema language (2003), Home page at http://www.relaxng.org/
Théry, L.: Formal proof authoring: An experiment. In: Informal Proc. User Interfaces for Theorem Provers, UITP 2003 (2003)
Trybulec, A., et al.: The Mizar project. University of Bialystok, Poland (1973), See web page hosted at http://mizar.org
Wenzel, M.: Isar — a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, p. 167. Springer, Heidelberg (1999)
Wenzel, M.: Isabelle/Isar — a versatile environment for human-readable formal proof documents. PhD thesis, Technische Universität München (2001)
Winterstein, D., Aspinall, D., Lüth, C.: Proof General/Eclipse. In: User Interfaces for Theorem Provers UITP 2005 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aspinall, D., Lüth, C., Wolff, B. (2006). Assisted Proof Document Authoring. In: Kohlhase, M. (eds) Mathematical Knowledge Management. MKM 2005. Lecture Notes in Computer Science(), vol 3863. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11618027_5
Download citation
DOI: https://doi.org/10.1007/11618027_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31430-1
Online ISBN: 978-3-540-31431-8
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.