Logo PTI
Polish Information Processing Society
Logo FedCSIS

Annals of Computer Science and Information Systems, Volume 12

Position Papers of the 2017 Federated Conference on Computer Science and Information Systems

Topological structures as a tool for formal modelling of rough sets

,

DOI: http://dx.doi.org/10.15439/2017F553

Citation: Position Papers of the 2017 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 12, pages 11–18 ()

Full text

Abstract. In the paper, 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. The paper 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.

References

  1. Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pąk, K., and Urban, J. (2015). Mizar: State-of-the-art and beyond. In Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., and Sorge, V., editors. Intelligent Computer Mathematics – International Conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings, volume 9150 of Lecture Notes in Computer Science. Springer, pages 261–279. http://dx.doi.org/10.1007/978-3-319-20615-8_17
  2. Bancerek G, Rudnicki P. (2002). A Compendium of Continuous Lattices in Mizar (formalizing recent mathematics). Journal of Automated Reasoning, 29(3/4):189–224. http://dx.doi.org/DOI: 10.1023/A:1021966832558
  3. Blanchette, J., Haslbeck, M., Matichuk, D., and Nipkow, T. (2015). Mining the Archive of Formal Proofs, in Kerber, M., editor. Conference on Intelligent Computer Mathematics (CICM 2015), Lecture Notes in Computer Science, 9150, pages 3–17, Springer. http://dx.doi.org/10.1007/978-3-319-20615-8_1
  4. Coghetto, R. (2016). Quasi-uniform space. Formalized Mathenatics, 24(3):215–226. http://dx.doi.org/10.1515/forma-2016-0017
  5. Coghetto, R. (2016). Uniform space. Formalized Mathenatics, 24(3):205–214. http://dx.doi.org/10.1515/forma-2016-0018
  6. Engelking, R. (1977). General Topology, volume 60 of Monografie Matematyczne. PWN – Polish Scientific Publishers, Warsaw.
  7. Gierz, G., Hofmann, K., Keimel, K., Lawson, J., Mislove, M., and Scott, D. (1980). A Compendium of Continuous Lattices. Springer-Verlag, Berlin, Heidelberg, New York.
  8. Grabowski, A. (2004). Solving two problems in general topology via types. In Filliâtre, J., Paulin-Mohring, C., and Werner, B., editors, Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15–18, 2004, Revised Selected Papers, volume 3839 of Lecture Notes in Computer Science, pages 138–153. Springer. http://dx.doi.org/10.1007/11617990_9
  9. Grabowski, A. (2005). On the computer-assisted reasoning about rough sets. In Dunin-Kȩplicz, B., Jankowski, A., Skowron, A., and Szczuka, M., editors, International Workshop on Monitoring, Security, and Rescue Techniques in Multiagent Systems Location, volume 28 of Advances in Soft Computing, pages 215–226, Berlin, Heidelberg. Springer-Verlag. http://dx.doi.org/10.1007/3-540-32370-8_15
  10. Grabowski, A. (2013). Automated discovery of properties of rough sets. Fundamenta Informaticae, 128(1-2):65–79. http://dx.doi.org/10.3233/FI-2013-933
  11. Grabowski, A. (2014). Efficient rough set theory merging. Fundamenta Informaticae, 135(4):371–385. http://dx.doi.org/10.3233/FI-2014-1129
  12. Grabowski, A. (2015). Mechanizing complemented lattices within Mizar type system. Journal of Automated Reasoning, 55(3):211–221. http://dx.doi.org/10.1007/s10817-015-9333-5
  13. Grabowski, A. (2016). Lattice theory for rough sets – a case study with Mizar, Fundamenta Informaticae, 147(2–3):223-240. http://dx.doi.org/10.3233/FI-2016-1406
  14. Grabowski, A. (2017). Computer certification of generalized rough sets based on relations. Accepted to International Joint Conference on Rough Sets, IJCRS 2017. http://dx.doi.org/10.1007/978-3-319-60837-2_7
  15. Grabowski, A., Korniłowicz, A., and Naumowicz, A. (2015). Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198. http://dx.doi.org/10.1007/s10817-015-9345-1
  16. Grabowski, A., Korniłowicz, A., and Schwarzweller, C. (2015). Equality in computer proof-assistants. In Ganzha, M., Maciaszek, L. A., and Paprzycki, M., editors, Proceedings of the 2015 Federated Conference on Computer Science and Information Systems, volume 5 of Annals of Computer Science and Information Systems, pages 45–54. IEEE. http://dx.doi.org/10.15439/2015F229
  17. Grabowski, A., Korniłowicz, A., Schwarzweller, C. (2016). On algebraic hierarchies in mathematical repository of Mizar. In: M. Ganzha, L.A. Maciaszek, M. Paprzycki, editors, Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, volume 8 of Annals of Computer Science and Information Systems, pages 363–371. IEEE. http://dx.doi.org/10.15439/2016F520
  18. Grabowski, A. and Moschner, M. (2004). Managing heterogeneous theories within a mathematical knowledge repository. In Asperti, A., Bancerek, G., and Trybulec, A., editors, Mathematical Knowledge Management, Third International Conference, MKM 2004, Bialowieza, Poland, September 19–21, 2004, Proceedings, volume 3119 of Lecture Notes in Computer Science, pages 116–129. Springer. http://dx.doi.org/10.1007/978-3-540-27818-4_9
  19. Grabowski, A. and Schwarzweller, C. (2007). Revisions as an essential tool to maintain mathematical repositories. In Proceedings of the 14th Symposium on Towards Mechanized Mathematical Assistants: 6th International Conference, Calculemus ’07 / MKM ’07, pages 235–249, Berlin, Heidelberg. Springer-Verlag. http://dx.doi.org/10.1007/978-3-540-73086-6_20
  20. Hammer, P.C. (1963). Extended topology: the continuity concept. Mathematics Magazine, 36(2):101–105.
  21. Iancu, M., Kohlhase, M., Rabe, F., and Urban, J. (2013). The Mizar Mathematical Library in OMDoc: Translation and applications. Journal of Automated Reasoning, 50(2):191–202. http://dx.doi.org/10.1007/s10817-012-9271-4
  22. Imura, H. and Eguchi, M. (1992). Finite topological spaces. Formalized Mathematics, 3(2):189–193.
  23. Järvinen, J. (2007). Lattice theory for rough sets, Transactions on Rough Sets VI, Lecture Notes in Computer Science (LNAI) 4374:400–498. http://dx.doi.org/10.1007/978-3-540-71200-8_22
  24. Korniłowicz, A. (2015). Definitional expansions in Mizar. Journal of Automated Reasoning, 55(3):257–268. http://dx.doi.org/10.1007/s10817-015-9331-7
  25. Korniłowicz, A. (2015). Flexary connectives in Mizar. Computer Languages, Systems & Structures, 44:238–250. http://dx.doi.org/10.1016/j.cl.2015.07.002
  26. Naumowicz, A. (2015). Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver. Journal of Automated Reasoning, 55(3):285–294. http://dx.doi.org/10.1007/s10817-015-9332-6
  27. Naumowicz, A. (2015). Tools for MML environment analysis. In Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., and Sorge, V., editors (2015). Intelligent Computer Mathematics – International Conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings, volume 9150 of Lecture Notes in Computer Science. Springer, pages 348–352. http://dx.doi.org/10.1007/978-3-319-20615-8_26
  28. Pawlak, Z. (1982). Rough sets. International Journal of Parallel Programming, 11:341–356.
  29. Pąk, K. (2015). Improving legibility of formal proofs based on the close reference principle is NP-hard. Journal of Automated Reasoning, 55(3):295–306. http://dx.doi.org/10.1007/s10817-015-9337-1
  30. Trybulec, A., Korniłowicz, A., Naumowicz, A., and Kuperberg, K. (2013). Formal mathematics for mathematicians. Journal of Automated Reasoning, 50(2):119–121. http://dx.doi.org/10.1007/s10817-012-9268-z
  31. Urban, J., Rudnicki, P., and Sutcliffe, G. (2013). ATP and presentation service for Mizar formalizations. Journal of Automated Reasoning, 50(2):229–241. http://dx.doi.org/10.1007/s10817-012-9269-y
  32. Vlach, M. (2008). Topologies of approximation spaces of rough set theory, In Interval/Probabilistic Uncertainty and Non-Classical Logics, pp. 176–186, Advances in Soft Computing, 46, Springer. http://dx.doi.org/10.1007/978-3-540-77664-2_14
  33. Weil, A. (1937). Sur les espaces a structure uniforme et sur la topologie generale. Act. Sci. Ind., 551, Paris.
  34. Yao, Y., Yao, B. (2012). Covering based rough set approximations, Information Sciences, 200:91–107. http://dx.doi.org/10.1016/j.ins.2012.02.065
  35. Zhu, W. (2007). Generalized rough sets based on relations, Information Sciences, 177(22):4997–5011. http://dx.doi.org/10.1016/j.ins.2007.05.037
  36. Zhu, W. (2007). Topological approaches to covering rough sets, Information Sciences, 177(6):1499–1508. http://dx.doi.org/10.1016/j.ins.2006.06.009