Skip to main content
SpringerLink
Log in

Extending Formal Topology in Mizar by Uniform Spaces

  • Chapter
  • First Online:
AI Aspects in Reasoning, Languages, and Computation

Part of the book series: Studies in Computational Intelligence ((SCI,volume 889))

Abstract

We present the topological counterpart supporting rich formal apparatus describing properties of rough sets within one of the largest repositories of computerized mathematical knowledge, the Mizar Mathematical Library. This chapter develops third and final (after lattice theory and the theory of general binary relations) planned path designed to be linked (via mechanisms of theory merging) with the theory of structures described by Pawlak in the early seventies of the previous century. We propose the revision of the existing topological apparatus offered by Mizar, and give the outline of the formalization of uniform spaces, important objects allowing for further representation of approximation spaces.

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 119.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 159.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 159.99
Price excludes VAT (USA)
  • Durable hardcover 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

References

  1. Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pa̧k, K., Urban, J.: Mizar: State-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) Intelligent Computer Mathematics – International Conference, CICM 2015, Washington, DC, USA, July 13–17, 2015. Proceedings. Lecture Notes in Computer Science, vol. 9150, pp. 261–279. Springer (2015). https://doi.org/10.1007/978-3-319-20615-8_17

    Google Scholar 

  2. Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pa̧k, K.: The role of the Mizar Mathematical Library for interactive proof development in Mizar. J. Autom. Reason. 61(1), 9–32 (2018). https://doi.org/10.1007/s10817-017-9440-6

    Article  MathSciNet  Google Scholar 

  3. Bancerek, G., Rudnicki, P.: A Compendium of Continuous Lattices in Mizar (formalizing recent mathematics). J. Autom. Reason. 29(3/4), 189–224 (2002). https://doi.org/10.1023/A:1021966832558

    Article  MathSciNet  Google Scholar 

  4. Blanchette, J., Haslbeck, M., Matichuk, D., Nipkow, T.: Mining the Archive of Formal Proofs. In: Kerber, M. (ed.) Conference on Intelligent Computer Mathematics (CICM 2015). Lecture Notes in Computer Science, vol. 9150, pp. 3–17, Springer (2015). https://doi.org/10.1007/978-3-319-20615-8_1

    Google Scholar 

  5. Coghetto, R.: Quasi-uniform space. Form. Math. 24(3), 205–214 (2016). https://doi.org/10.1515/forma-2016-0017

    Article  Google Scholar 

  6. Coghetto, R.: Uniform space. Form. Math. 24(3), 215–226 (2016). https://doi.org/10.1515/forma-2016-0018

    Article  Google Scholar 

  7. Engelking, R.: General Topology, Monografie Matematyczne, vol. 60. PWN—Polish Scientific Publishers, Warsaw (1977)

    Google Scholar 

  8. Gierz, G., Hofmann, K., Keimel, K., Lawson, J., Mislove, M., Scott, D.: A Compendium of Continuous Lattices. Springer, Berlin (1980)

    Book  Google Scholar 

  9. Gomolińska, A.: A comparative study of some generalized rough approximations. Fundam. Inform. 51, 103–119 (2002)

    MathSciNet  MATH  Google Scholar 

  10. Grabowski, A.: Solving two problems in general topology via types. In: Filliâtre, J., Paulin-Mohring, C., Werner., B. (eds.) Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15–18, 2004. Revised Selected Papers. Lecture Notes in Computer Science, vol. 3839, pp. 138–153 (2004). Springer. https://doi.org/10.1007/11617990_9

    Google Scholar 

  11. Grabowski, A.: On the computer-assisted reasoning about rough sets. In: Dunin-Kȩplicz, B., Jankowski, A., Skowron, A., Szczuka., M. (eds.) International Workshop on Monitoring, Security, and Rescue Techniques in Multiagent Systems Location. Advances in Soft Computing, vol. 28, pp. 215–226. Springer, Berlin (2005). https://doi.org/10.1007/3-540-32370-8_15

  12. Grabowski, A.: Automated discovery of properties of rough sets. Fundam. Inform. 128(1–2), 65–79 (2013). https://doi.org/10.3233/FI-2013-933

    Article  MathSciNet  MATH  Google Scholar 

  13. Grabowski, A.: Efficient rough set theory merging. Fundam. Inform. 135(4), 371–385 (2014). https://doi.org/10.3233/FI-2014-1129

    Article  MathSciNet  MATH  Google Scholar 

  14. Grabowski, A.: Mechanizing complemented lattices within Mizar type system. J. Autom. Reason. 55(3), 211–221 (2015). https://doi.org/10.1007/s10817-015-9333-5

    Article  MathSciNet  MATH  Google Scholar 

  15. Grabowski, A.: Lattice theory for rough sets—a case study with Mizar. Fundam. Inform. 147(2–3), 223–240 (2016). https://doi.org/10.3233/FI-2016-1406

    Article  MathSciNet  Google Scholar 

  16. Grabowski, A.: Computer certification of generalized rough sets based on relations. In: Polkowski, L., Yao, Y., Artiemjew, P., Ciucci, D., Liu, D., Ślȩzak, D., Zielosko, B. (eds.) Rough Sets, International Joint Conference on Rough Sets, IJCRS 2017. Lecture Notes in Artificial Intelligence, vol. 10313, pp. 83–94. Springer (2017). https://doi.org/10.1007/978-3-319-60837-2_7

    Chapter  Google Scholar 

  17. Grabowski, A., Coghetto, R.: Topological structures as a tool for formal modelling of rough sets. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Position Papers of the 2017 Federated Conference on Computer Science and Information Systems. Annals of Computer Science and Information Systems, vol. 12, pp. 11–18. IEEE (2017). https://doi.org/10.15439/2017F553

  18. Grabowski, A., Korniłowicz, A., Naumowicz, A.: Four decades of Mizar. J. Autom. Reason. 55(3), 191–198 (2015). https://doi.org/10.1007/s10817-015-9345-1

    Article  MathSciNet  MATH  Google Scholar 

  19. Grabowski, A., Korniłowicz, A., Schwarzweller, C.: Equality in computer proof-assistants. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the 2015 Federated Conference on Computer Science and Information Systems. Annals of Computer Science and Information Systems, vol. 5, pp. 45–54. IEEE (2015). https://doi.org/10.15439/2015F229

  20. Grabowski, A., Korniłowicz, A., Schwarzweller, C.: On algebraic hierarchies in mathematical repository of Mizar. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the 2016 Federated Conference on Computer Science and Information Systems. Annals of Computer Science and Information Systems, vol. 8, pp. 363–371. IEEE (2016). https://doi.org/10.15439/2016F520

  21. Grabowski, A., Moschner, M.: Managing heterogeneous theories within a mathematical knowledge repository. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) Mathematical Knowledge Management, Third International Conference, MKM 2004, Bialowieza, Poland, September 19–21, 2004. Proceedings. Lecture Notes in Computer Science, vol. 3119, pp. 116–129. Springer (2004). https://doi.org/10.1007/978-3-540-27818-4_9

    Google Scholar 

  22. Grabowski, A., Schwarzweller, C.: Revisions as an essential tool to maintain mathematical repositories. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Towards Mechanized Mathematical Assistants, 6th International Conference, MKM 2007, Calculemus 2007. Lecture Notes in Computer Science, vol. 4573, pp. 235–249. Springer, Berlin (2007). https://doi.org/10.1007/978-3-540-73086-6_20

    Chapter  Google Scholar 

  23. Hammer, P.C.: Extended topology: the continuity concept. Math. Mag. 36(2), 101–105 (1963)

    Article  MathSciNet  Google Scholar 

  24. Iancu, M., Kohlhase, M., Rabe, F., Urban, J.: The Mizar Mathematical Library in OMDoc: Translation and applications. J. Autom. Reason. 50(2), 191–202 (2013). https://doi.org/10.1007/s10817-012-9271-4

    Article  MathSciNet  MATH  Google Scholar 

  25. Imura, H., Eguchi, M.: Finite topological spaces. Form. Math. 3(2), 189–193 (1992)

    Google Scholar 

  26. Järvinen, J.: Lattice theory for rough sets. In: Transactions on Rough Sets VI. Lecture Notes in Computer Science (LNAI), vol. 4374, pp. 400–498 (2007). https://doi.org/10.1007/978-3-540-71200-8_22

  27. Korniłowicz, A.: Definitional expansions in Mizar. J. Autom. Reason. 55(3), 257–268 (2015). https://doi.org/10.1007/s10817-015-9331-7

    Article  MathSciNet  MATH  Google Scholar 

  28. Lee, G., Rudnicki, P.: Alternative aggregates in Mizar. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Towards Mechanized Mathematical Assistants, MKM 2007, Calculemus 2007. Lecture Notes in Computer Science, vol. 4573, pp. 327–341. Springer (2007). https://doi.org/10.1007/978-3-540-73086-6_26

  29. Liu, G., Fuwa, Y., Eguchi, M.: Formal topological spaces. Form. Math. 9(3), 537–543 (2001)

    Google Scholar 

  30. 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). https://doi.org/10.1007/s10817-015-9332-6

    Article  MathSciNet  MATH  Google Scholar 

  31. Naumowicz, A.: Tools for MML environment analysis. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) Intelligent Computer Mathematics – International Conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9150, pp. 348–352. Springer (2015). https://doi.org/10.1007/978-3-319-20615-8_26

    Google Scholar 

  32. Pawlak, Z.: Rough sets. Int. J. Parallel Program. 11, 341–356 (1982)

    MATH  Google Scholar 

  33. Pa̧k, K.: Improving legibility of formal proofs based on the close reference principle is NP-hard. J. Autom. Reason. 55(3), 295–306 (2015). https://doi.org/10.1007/s10817-015-9337-1

    Article  MathSciNet  Google Scholar 

  34. Trybulec, A., Korniłowicz, A., Naumowicz, A., Kuperberg, K.: Formal mathematics for mathematicians. J. Autom. Reason. 50(2), 119–121 (2013). https://doi.org/10.1007/s10817-012-9268-z

    Article  Google Scholar 

  35. Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reason. 50(2), 229–241 (2013). https://doi.org/10.1007/s10817-012-9269-y

    Article  MathSciNet  MATH  Google Scholar 

  36. Vlach, M.: Topologies of approximation spaces of rough set theory. In: Huynh, V.N., Nakamori, Y., Ono, Y., Lawry, J., Kreinovich, V., Nguyen, H.T. (eds.) Interval/Probabilistic Uncertainty and Non-Classical Logics. Advances in Soft Computing, vol. 46, pp. 176–186. Springer (2008). https://doi.org/10.1007/978-3-540-77664-2_14

  37. Weil, A.: Sur les espaces a structure uniforme et sur la topologie generale. Actuar. Sci. India 551, Paris (1937)

    Google Scholar 

  38. Yao, Y., Yao, B.: Covering based rough set approximations. Inf. Sci. 200, 91–107 (2012). https://doi.org/10.1016/j.ins.2012.02.065

    Article  MathSciNet  MATH  Google Scholar 

  39. Zhu, W.: Generalized rough sets based on relations. Inf. Sci. 177(22), 4997–5011 (2007). https://doi.org/10.1016/j.ins.2007.05.037

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Informatics, University of Białystok, ul. Ciołkowskiego 1 M, 15-245, Białystok, Poland

    Adam Grabowski

  2. Rue de la Brasserie 5, 7100, La Louvière, Belgium

    Roland Coghetto

Authors
  1. Adam Grabowski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Roland Coghetto
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Adam Grabowski .

Editor information

Editors and Affiliations

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

    Adam Grabowski

  2. Department of Mathematics, Stockholm University, Stockholm, Sweden

    Roussanka Loukanova

  3. Institute of Informatics, University of Gdansk, Gdańsk, Poland

    Christoph Schwarzweller

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Grabowski, A., Coghetto, R. (2020). Extending Formal Topology in Mizar by Uniform Spaces. In: Grabowski, A., Loukanova, R., Schwarzweller, C. (eds) AI Aspects in Reasoning, Languages, and Computation. Studies in Computational Intelligence, vol 889. Springer, Cham. https://doi.org/10.1007/978-3-030-41425-2_3

Download citation

Publish with us

Policies and ethics

Search

Navigation