Skip to main content
SpringerLink
Log in
Book cover

International Conference on Information Systems Architecture and Technology

ISAT 2017: Information Systems Architecture and Technology: Proceedings of 38th International Conference on Information Systems Architecture and Technology – ISAT 2017 pp 166–175Cite as

Towards Standardized Mizar Environments

  • Conference paper
  • First Online:

Part of the book series: Advances in Intelligent Systems and Computing ((AISC,volume 656))

Abstract

The effectiveness of formalizing substantial parts of mathematics largely depends on the availability of relevant background knowledge. The bigger the knowledge library, however, the harder it is to specify what is or should be relevant. Even with today’s size of the libraries available for various proof assistants, importing the whole library is not an option for practical performance reasons. On the other hand, too detailed import mechanisms are prone to dependency problems and pose certain difficulty for the user. In this paper we present the key ideas of a project aimed at generating standardized formalization environments which could be used to facilitate developing new formalizations based on the current content of the Mizar Mathematical Library. Showing the results of this research based on the library designed with great focus on reusability can also be insightful for designers of other formalization systems and libraries.

This is a preview of subscription content, 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   129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   169.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

Learn about institutional subscriptions

Notes

  1. 1.

    http://mizar.org.

  2. 2.

    The processing and analysis of the Mizar library has been performed using the infrastructure of the University of Bialystok High Performance Computing Center.

  3. 3.

    MML ver. 5.41.1289 distributed with the compatible Mizar system ver. 8.1.06, http://mizar.uwb.edu.pl/system/#download.

  4. 4.

    According to the statistics provided by MML Query, http://fm.uwb.edu.pl/mmlquery/fillin.php?filledfilename=statistics.mqt&argument=number+1&version=5.40.1289.

References

  1. Harrison, J.: HOL Light tutorial. http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf. Accessed 18 May 2017

  2. Bertot, Y., Castéran, P.: Interactive theorem proving and program development - Coq’Art: the calculus of inductive constructions. In: Texts in Theoretical Computer Science. An EATCS Series. Springer (2004)

    Google Scholar 

  3. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283. Springer, New York (2002)

    MATH  Google Scholar 

  4. Grabowski, A., Korniłowicz, A., Naumowicz, A.: Four decades of Mizar. J. Autom. Reason. 55(3), 191–198 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  5. Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pąk, K., Urban, J.: Mizar: state-of-the-art and beyond. In: [24], pp. 261–279 (2015)

    Google Scholar 

  6. Alama, J.: Mizar-items: exploring fine-grained dependencies in the Mizar Mathematical Library. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and Proceedings of 10th International Conference, MKM 2011, Bertinoro, Italy, 18–23 July 2011. Lecture Notes in Computer Science, vol. 6824, pp. 276–277. Springer (2011)

    Google Scholar 

  7. Blanchette, J.C., Haslbeck, M., Matichuk, D., Nipkow, T.: Mining the Archive of formal proofs. In: [24], pp. 3–17 (2015)

    Google Scholar 

  8. Czuba, S.T.: Schemes. Formaliz. Math. 2(3), 385–391 (1991)

    Google Scholar 

  9. Korniłowicz, A.: Jordan curve theorem. Formaliz. Math. 13(4), 481–491 (2005)

    Google Scholar 

  10. Trybulec, Z.: Properties of subsets. Formaliz. Math. 1(1), 67–71 (1990)

    Google Scholar 

  11. Grabowski, A., Korniłowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formaliz. Reason. 3(2), 153–245 (2010)

    MathSciNet  MATH  Google Scholar 

  12. Naumowicz, A.: Enhanced processing of adjectives in Mizar. Stud. Log. Gramm. Rhetor. 18(31), 89–101 (2009)

    Google Scholar 

  13. Korniłowicz, A.: On rewriting rules in Mizar. J. Autom. Reason. 50(2), 203–210 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  14. Grabowski, A., Korniłowicz, A., Schwarzweller, C.: Equality in computer proof-assistants. In: 2015 Federated Conference on Computer Science and Information Systems, FedCSIS 2015, Łódź, Poland, 13–16 September 2015, pp. 45–54 (2015)

    Google Scholar 

  15. Korniłowicz, A.: Definitional expansions in Mizar. J. Autom. Reason. 55(3), 257–268 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  16. Naumowicz, A.: Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver. J. Autom. Reason. 55(3), 285–294 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  17. Naumowicz, A.: Interfacing external CA systems for Gröbner bases computation in Mizar proof checking. Int. J. Comput. Math. 87(1), 1–11 (2010)

    Article  MATH  Google Scholar 

  18. Byliński, C.: Cartesian categories. Formaliz. Math. 3(2), 161–169 (1992)

    Google Scholar 

  19. Trybulec, Z., Święczkowska, H.: Boolean properties of sets. Formaliz. Math. 1(1), 17–23 (1990)

    Google Scholar 

  20. Naumowicz, A.: Tools for MML environment analysis. In: [24], pp. 348–352 (2015)

    Google Scholar 

  21. Bancerek, G., Rudnicki, P.: A compendium of continuous lattices in Mizar. J. Autom. Reason. 29(3–4), 189–224 (2002)

    Article  MATH  Google Scholar 

  22. Korniłowicz, A.: Cartesian products of relations and relational structures. Formaliz. Math. 6(1), 145–152 (1997)

    Google Scholar 

  23. Bancerek, G.: Bases and refinements of topologies. Formaliz. Math. 7(1), 35–43 (1998)

    Google Scholar 

  24. Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.): Intelligent Computer Mathematics - International Conference, CICM 2015, Proceedings. Washington, DC, USA, 13–17 July 2015. Lecture Notes in Computer Science, vol. 9150. Springer (2015)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Informatics, University of Bialystok, Bialystok, Poland

    Adam Naumowicz

Authors
  1. Adam Naumowicz
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Adam Naumowicz .

Editor information

Editors and Affiliations

  1. Department of Computer Science, Faculty of Computer Science and Management, Wrocław University of Science and Technology, Wrocław, Poland

    Jerzy Świątek

  2. Department of Computer Science, Faculty of Computer Science and Management, Wrocław University of Science and Technology, Wrocław, Poland

    Leszek Borzemski

  3. Department of Management Systems, Faculty of Computer Science and Management, Wrocław University of Science and Technology, Wrocław, Poland

    Zofia Wilimowska

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Cite this paper

Naumowicz, A. (2018). Towards Standardized Mizar Environments. In: Świątek, J., Borzemski, L., Wilimowska, Z. (eds) Information Systems Architecture and Technology: Proceedings of 38th International Conference on Information Systems Architecture and Technology – ISAT 2017. ISAT 2017. Advances in Intelligent Systems and Computing, vol 656. Springer, Cham. https://doi.org/10.1007/978-3-319-67229-8_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67229-8_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67228-1

  • Online ISBN: 978-3-319-67229-8

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation