Automated Comparative Study of Some Generalized Rough Approximations

• Autorzy: Grabowski Adam

Identyfikatory

DOI

10.3233/FI-2021-2019

• Języki publikacji: EN

Abstrakty

EN

The paper contains some remarks on building automated counterpart of a comparison of some generalized rough approximations of sets, where the classical indiscernibility relation is generalized to arbitrary binary relation. Our focus was on translating rationality postulates for such operators by means of the Mizar system – the software and the database which allows for expressing and checking mathematical knowledge for the logical correctness. The main objective was the formal (and machine-checked) proof of Theorem 4.1 from A. Gomolińska’s paper “A Comparative Study of Some Generalized Rough Approximations ”, hence the present title. We provide also the discussion on how to make the presentation more efficient to reuse the reasoning techniques of the Mizar verifier.

Słowa kluczowe

EN

formalization of mathematics; Mizar Mathematical Library; rough approximation

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 179, nr 2
• Strony: 165--182
• Opis fizyczny: Bibliogr. 28 poz., tab.

Twórcy

autor

Grabowski Adam

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

Bibliografia

• [1] Pawlak Z. Rough Sets: Theoretical Aspects of Reasoning about Data. Kluwer, Dordrecht, 1991. doi:10.1007/978-94-011-3534-4.
• [2] Skowron A, Stepaniuk J. Tolerance approximation spaces. Fundamenta Informaticae, 1996. 27(2/3):245-253. doi:10.3233/FI-1996-272311.
• [3] Yao Y. Two views of the theory of rough sets in finite universes. International Journal of Approximate Reasoning, 1996. 15(4):291-317. doi:10.1016/S0888-613X(96)00071-0.
• [4] Zhu W. Generalized rough sets based on relations. Information Sciences, 2007. 177(22):4997-5011. doi:10.1016/j.ins.2007.05.037.
• [5] Yao Y, Yao B. Covering based rough set approximations. Information Sciences, 2012. 200:91-107. doi:10.1016/j.ins.2012.02.065.
• [6] Ma Z, Li J, Mi J. Some minimal axioms sets of rough sets. Information Sciences, 2015. 312:40-54. doi:10.1016/j.ins.2015.03.052.
• [7] Gomolińska A. A comparative study of some generalized rough approximations. Fundamenta Informaticae, 2002. 51(1-2):103-119.
• [8] Bryniarski E. Formal conception of rough sets. Fundamenta Informaticae, 1996. 27(2/3):109-136. doi:10.3233/FI-1996-272302.
• [9] Wiedijk F. Formal proof - getting started. Notices of the American Mathematical Society, 2008. 55(11):1408-1414.
• [10] Bancerek G, Byliński C, Grabowski A, Korniłowicz A, Matuszewski R, Naumowicz A, Pąk K. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 2018. 61(1):9-32. doi:10.1007/s10817-017-9440-6.
• [11] Naumowicz A. Automating boolean set operations in Mizar proof checking with the aid of an external SAT solver. Journal of Automated Reasoning, 2015. 55:285-294. doi:10.1007/s10817-015-9332-6.
• [12] Blanchette J, Haslbeck M, Matichuk D, Nipkow T. Mining the Archive of Formal Proofs. In: Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2015 pp. 3-17. doi:10.1007/978-3-319-20615-8_1.
• [13] Grabowski A, Schwarzweller C. Rough Concept Analysis - theory development in the Mizar system. In: Asperti A, Bancerek G, Trybulec A (eds.), Mathematical Knowledge Management, Third International Conference, MKM 2004, Bialowieza, Poland, September 19-21, 2004, Proceedings, volume 3119 of Lecture Notes in Computer Science. Springer, Berlin, Heidelberg, 2004 pp. 130-144. doi:10.1007/978-3-540-27818-4_10.
• [14] Pomykała J. Approximation operations in approximation space. Bull. Polish Acad. Sci. Math., 1987. 35(9-10):653-662.
• [15] Grabowski A. Lattice Theory for Rough Sets - a case study with Mizar. Fundamenta Informaticae, 2016. 147(2-3):223-240. doi:10.3233/FI-2016-1406.
• [16] Grabowski A, Jastrzębska M. A note on a formal approach to rough operators. In: Szczuka M, Kryszkiewicz M, Ramanna S, Jensen R, Hu Q (eds.), Rough Sets and Current Trends in Computing - 7th International Conference, RSCTC 2010, Warsaw, Poland, June 28-30, 2010. Proceedings, volume 6086 of Lecture Notes in Computer Science. Springer, Berlin, Heidelberg, 2010 pp. 307-316. doi:10.1007/978-3-642-13529-3_33.
• [17] Grabowski A. Automated discovery of properties of rough sets. Fundamenta Informaticae, 2013. 128:65-79. doi:10.3233/FI-2013-933.
• [18] Polkowski L. Rough mereology. In: Approximate Reasoning by Parts, volume 20 of Intelligent Systems Reference Library. Springer, Berlin, Heidelberg, 2011 pp. 229-257. doi:10.1007/978-3-642-22279-5_6.
• [19] Grabowski A. Building a framework of rough inclusion functions by means of computerized proof assistant. In: Mihálydeák T, Min F, Wang G, Banerjee M, Düntsch I, Suraj Z, Ciucci D (eds.), Rough Sets, volume 11499 of Lecture Notes in Computer Science. Springer International Publishing, Cham, 2019 pp. 225-238. doi:10.1007/978-3-030-22815-6_18.
• [20] 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, volume 10313 of Lecture Notes in Computer Science. Springer International Publishing, Cham, 2017 pp. 83-94. doi:10.1007/978-3-319-60837-2_7.
• [21] Grabowski A, Korniłowicz A, Naumowicz A. Four decades of Mizar. Journal of Automated Reasoning, 2015. 55(3):191-198. doi:10.1007/s10817-015-9345-1.
• [22] Grabowski A. Efficient rough set theory merging. Fundamenta Informaticae, 2014. 135(4):371-385. doi:10.3233/FI-2014-1129.
• [23] Jiang B, Qin K, Pei Z. On transitive uncertainty mappings. In: Yao J, Lingras P, Wu WZ, Szczuka M, Cercone NJ, Ślęzak D (eds.), Rough Sets and Knowledge Technology, volume 4481 of Lecture Notes in Computer Science. Springer, Berlin, Heidelberg, 2007 pp. 42-49. doi:10.1007/978-3-540-72458-2_5.
• [24] Bonikowski Z. Unit operation in approximation spaces. In: Szczuka M, Kryszkiewicz M, Ramanna S, Jensen R, Hu Q (eds.), Rough Sets and Current Trends in Computing - 7th International Conference, RSCTC 2010, Warsaw, Poland, June 28-30, 2010. Proceedings, volume 6086 of Lecture Notes in Computer Science. Springer, Berlin, Heidelberg, 2010 pp. 337-346. doi:10.1007/978-3-642-13529-3_36.
• [25] Grabowski A. Fundamental properties of fuzzy implications. Formalized Mathematics, 2018. 26(4):271-276. doi:10.2478/forma-2018-0023.
• [26] Grabowski A, Sielwiesiuk M. Formalizing two generalized approximation operators. Formalized Mathematics, 2018. 26(2):183-191. doi:10.2478/forma-2018-0016.
• [27] Grabowski A. Mechanizing complemented lattices within Mizar system. Journal of Automated Reasoning, 2015. 55:211-221. doi:10.1007/s10817-015-9333-5.
• [28] Gomolińska A. On certain rough inclusion functions. In: Peters JF, Skowron A, Rybiński H (eds.), Transactions on Rough Sets IX, volume 5390 of Lecture Notes in Computer Science. Springer, Berlin, Heidelberg, 2008 pp. 35-55. doi:10.1007/978-3-540-89876-4_3.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).