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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
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
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
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
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
Coghetto, R.: Quasi-uniform space. Form. Math. 24(3), 205–214 (2016). https://doi.org/10.1515/forma-2016-0017
Coghetto, R.: Uniform space. Form. Math. 24(3), 215–226 (2016). https://doi.org/10.1515/forma-2016-0018
Engelking, R.: General Topology, Monografie Matematyczne, vol. 60. PWN—Polish Scientific Publishers, Warsaw (1977)
Gierz, G., Hofmann, K., Keimel, K., Lawson, J., Mislove, M., Scott, D.: A Compendium of Continuous Lattices. Springer, Berlin (1980)
Gomolińska, A.: A comparative study of some generalized rough approximations. Fundam. Inform. 51, 103–119 (2002)
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
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
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
Grabowski, A.: Efficient rough set theory merging. Fundam. Inform. 135(4), 371–385 (2014). https://doi.org/10.3233/FI-2014-1129
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
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
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
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
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
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
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
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
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
Hammer, P.C.: Extended topology: the continuity concept. Math. Mag. 36(2), 101–105 (1963)
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
Imura, H., Eguchi, M.: Finite topological spaces. Form. Math. 3(2), 189–193 (1992)
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
Korniłowicz, A.: Definitional expansions in Mizar. J. Autom. Reason. 55(3), 257–268 (2015). https://doi.org/10.1007/s10817-015-9331-7
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
Liu, G., Fuwa, Y., Eguchi, M.: Formal topological spaces. Form. Math. 9(3), 537–543 (2001)
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
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
Pawlak, Z.: Rough sets. Int. J. Parallel Program. 11, 341–356 (1982)
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
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
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
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
Weil, A.: Sur les espaces a structure uniforme et sur la topologie generale. Actuar. Sci. India 551, Paris (1937)
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
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
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
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
DOI: https://doi.org/10.1007/978-3-030-41425-2_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-41424-5
Online ISBN: 978-3-030-41425-2
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)