Skip to main content
SpringerLink
Log in

On Duplication in Mathematical Repositories

  • Conference paper
Intelligent Computer Mathematics (CICM 2010)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6167))

Included in the following conference series:

Abstract

Building a repository of proof-checked mathematical knowledge is without any doubt a lot of work, and besides the actual formalization process there is also the task of maintaining the repository. Thus it seems obvious to keep a repository as small as possible, in particular each piece of mathematical knowledge should be formalized only once.

In this paper, however, we claim that it might be reasonable or even necessary to duplicate knowledge in a mathematical repository. We analyze different situations and reasons for doing so, provide a number of examples supporting our thesis and discuss some implications for building mathematical repositories.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. The Coq Proof Assistant, http://coq.inria.fr

  2. Davenport, J.H.: MKM from Book to Computer: A Case Study. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol. 2594, pp. 17–29. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  3. de Bruijn, N.G.: The Mathematical Vernacular, a language for mathematics with typed sets. In: Dybjer, P., et al. (eds.) Proceedings of the Workshop on Programming Languages, Marstrand, Sweden (1987)

    Google Scholar 

  4. von zur Gathen, J., Gerhard, J.: Modern Computer Algebra. Cambridge University Press, Cambridge (1999)

    MATH  Google Scholar 

  5. Grabowski, A., Schwarzweller, C.: Translating Mathematical Vernacular into Knowledge Repositories. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol. 3863, pp. 49–64. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  6. Harrison, J.: The HOL Light Theorem Prover, http://www.cl.cam.ac.uk/~jrh13/hol-light

  7. Hurd, J.: Verification of the Miller-Rabin Probabilistic Primality Test. Journal of Logic and Algebraic Programming 50(1-2), 3–21 (2003)

    Article  MathSciNet  Google Scholar 

  8. Kapur, D., Zhang, H.: An Overview of Rewrite Rule Laboratory (RRL). In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 559–563. Springer, Heidelberg (1989)

    Google Scholar 

  9. Kamareddine, F., Nederpelt, R.: A Refinement of de Bruijn’s Formal Language of Mathematics. Journal of Logic, Language and Information 13(3), 287–340 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  10. Knuth, D.: The Art of Computer Programming. In: Seminumerical Algorithms, 3rd edn., vol. 2, Addison-Wesley, Reading (1997)

    Google Scholar 

  11. Kondracki, A.: The Chinese Remainder Theorem. Formalized Mathematics 6(4), 573–577 (1997)

    Google Scholar 

  12. Korniłowicz, A.: How to Define Terms in Mizar Effectively. Studies in Logic, Grammar and Rhetoric 18(31), 67–77 (2009)

    Google Scholar 

  13. Lüneburg, H.: Vorlesungen über Lineare Algebra, BI Wissenschaftsverlag (1993) (in German)

    Google Scholar 

  14. Ménissier-Morain, V.: A Proof of the Chinese Remainder Lemma, http://logical.saclay.inria.fr/coq/distrib/current/contribs/ZChinese.html

  15. The Mizar Home Page, http://mizar.org

  16. Naumowicz, A., Byliński, C.: Improving Mizar Texts with Properties and Requirements. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 290–301. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  17. Pollet, M., Sorge, V., Kerber, M.: Intuitive and Formal Representations: The Case of Matrices. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 317–331. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  18. Rudnicki, P., Trybulec, A.: Mathematical Knowledge Management in Mizar. In: Buchberger, B., Caprotti, O. (eds.) Proceedings of the 1st International Conference on Mathematical Knowledge Management, Linz, Austria (2001)

    Google Scholar 

  19. Schwarzweller, C.: Modular Integer Arithmetic. Formalized Mathematics 16(3), 247–252 (2008)

    Article  Google Scholar 

  20. Schwarzweller, C.: The Chinese Remainder Theorem, its Proofs and its Generalizations in Mathematical Repositories. Studies in Logic, Grammar and Rhetoric 18(31), 103–119 (2009)

    Google Scholar 

  21. Urban, J.: MoMM — Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics. International Journal on Artificial Intelligence Tools 15(1), 109–130 (2006)

    Article  Google Scholar 

  22. Wiedijk, F.: On the Usefulness of Formal Methods. In: Nieuwsbrief van de NVTI, pp. 14–23 (2006)

    Google Scholar 

  23. Zhang, H., Hua, X.: Proving the Chinese Remainder Theorem by the Cover Set Induction. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 431–455. Springer, Heidelberg (1992)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Mathematics, University of Białystok, ul. Akademicka 2, 15-267, Białystok, Poland

    Adam Grabowski

  2. Department of Computer Science, University of Gdańsk, ul. Wita Stwosza 57, 80-952, Gdańsk, Poland

    Christoph Schwarzweller

Authors
  1. Adam Grabowski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christoph Schwarzweller
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. German Research Center for Artificial Intelligence Bremen, Germany

    Serge Autexier

  2. Karlsruhe Institute of Technology, Germany

    Jacques Calmet

  3. CEDRIC/CNAM, Paris, France

    David Delahaye

  4. American Mathematical Society, Ann Arbor, USA

    Patrick D. F. Ion

  5. INRIA Sophia-Antipolis, France

    Laurence Rideau

  6. École Nationale Supérieure d’Informatique pour l’industrie et l’Entreprise, Evry, France

    Renaud Rioboo

  7. School of Computer Science, Edgbaston, University of Birmingham, B15 2TT, Birmingham, UK

    Alan P. Sexton

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Grabowski, A., Schwarzweller, C. (2010). On Duplication in Mathematical Repositories. In: Autexier, S., et al. Intelligent Computer Mathematics. CICM 2010. Lecture Notes in Computer Science(), vol 6167. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14128-7_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14128-7_26

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14127-0

  • Online ISBN: 978-3-642-14128-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation