From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls
- 276 Downloads
When we try to extract to an open format formal mathematical knowledge from libraries of already existing proof-assistants, we must face several problems and make important design decisions. This paper is based on our experiences on the exportation to XML of the theories developed in Coq and NuPRL: we try to collect a set of (hopefully useful) suggestions to pave the way to other teams willing to attempt the same operation.
KeywordsComputer Algebra System Logical Framework High Order Logic Atomic Component Abstract Data Type
Unable to display preview. Download preview PDF.
- 1.M. Agrawal, N. Kayal, N. Saxena, “PRIMES in P”, unpublished, August 2002, http://www.cse.iitk.ac.in/users/manindra/primality.ps.
- 2.A. Asperti, F. Guidi, L. Padovani, C. Sacerdoti Coen, I. Schena, “Mathematical Knowledge Management in HELM”, in On-Line Proceedings of the First International Workshop on Mathematical Knowledge Management (MKM2001), RISC-Linz, Austria, September 2001.Google Scholar
- 3.A. Asperti, L. Padovani, C. Sacerdoti Coen, Schena, I., “HELM and the semantic Math-Web”. Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLS 2001), 3–6 September 2001, Edinburgh, Scotland.Google Scholar
- 4.A. Asperti, B. Wegner, “MoWGLI-A New Approach for the Content Description in Digital Documents”, in Proceedings of the Ninth International Conference on Electronic Resources and the Social Role of Libraries in the Future, Section 4, Volume 1.Google Scholar
- 5.O. Caprotti, H. Geuvers, and M. Oostdijk, “Certified and Portable Mathematical Documents from Formal Contexts”, in On-Line Proceedings of the First International Workshop on Mathematical Knowledge Management (MKM2001), RISC-Linz, Austria, September 2001.Google Scholar
- 6.Y. Coscoy. “Explication textuelle de preuves pour le Calcul des Constructions Inductives”, Phd. Thesis, Université de Nice-Sophia Antipolis, 2000.Google Scholar
- 7.A. Franke, M. Kohlhase, “MBase: Representing Knowledge and Context for the Integration of Mathematical Software Systems”, to appear in Journal of Symbolic Computation.Google Scholar
- 8.J. Harrison, “Real Numbers in Real Applications”, invited talk at Formalising Continuous Mathematics 2002 (FCM2002), 19th August 2002, Radisson Hotel, Hampton, VA, USAGoogle Scholar
- 10.Learning Technology Standards Committee of IEEE, “Draft Standard for Learning Object Metadata”, July 15th 2002.Google Scholar
- 11.C. Muñoz, “Un calcul de substitutions pour la représentation de preuves partielles en théorie de types”, PhD. Thesis, University Paris 7, 1997.Google Scholar
- 12.The OpenMath Esprit Consortium, “The OpenMath Standard”, O. Caprotti, D. P. Carlisle, A. M. Cohen editors.Google Scholar