Advertisement

From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls

  • Claudio Sacerdoti Coen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2594)

Abstract

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.

Keywords

Computer Algebra System Logical Framework High Order Logic Atomic Component Abstract Data Type 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    M. Agrawal, N. Kayal, N. Saxena, “PRIMES in P”, unpublished, August 2002, http://www.cse.iitk.ac.in/users/manindra/primality.ps.
  2. 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. 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. 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. 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. 6.
    Y. Coscoy. “Explication textuelle de preuves pour le Calcul des Constructions Inductives”, Phd. Thesis, Université de Nice-Sophia Antipolis, 2000.Google Scholar
  7. 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. 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
  9. 9.
    M. Kohlhase, A. Franke, “MBase: Representing Knowledge and Context for the Integration of Mathematical Software Systems”, Journal of Symbolic Computation 23:4 (2001), pp. 365–402.MathSciNetCrossRefGoogle Scholar
  10. 10.
    Learning Technology Standards Committee of IEEE, “Draft Standard for Learning Object Metadata”, July 15th 2002.Google Scholar
  11. 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. 12.
    The OpenMath Esprit Consortium, “The OpenMath Standard”, O. Caprotti, D. P. Carlisle, A. M. Cohen editors.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Claudio Sacerdoti Coen
    • 1
  1. 1.Department of Computer ScienceBolognaItaly

Personalised recommendations