Lattice Theory for Rough Sets : A Case Study with Mizar

• Autorzy: Grabowski A.

Identyfikatory

DOI

10.3233/FI-2016-1406

• Konferencja: International Workshop on CONCURRENCY, SPECIFICATION, and PROGRAMMING (CS&P 2015), (24; 28-30.09.2015, Rzeszów, Poland).
• Języki publikacji: EN

Abstrakty

EN

Rough sets offer a well-known approach to incomplete or imprecise data. In the paper I briefly report how this framework was successfully encoded by means of one of the leading computer proof-assistants in the world. The general approach is essentially based on binary relations, and all natural properties of approximation operators can be obtained via adjectives added to underlying relations. I focus on lattice-theoretical aspects of rough sets to enable the application of external theorem provers like EQP or Prover9 as well as to translate them into TPTP format widely recognized in the world of automated proof search. I wanted to have a clearly written, possibly formal, although informal as a rule, paper authored by a specialist from the discipline another than lattice theory. It appeared that Lattice theory for rough sets by Jouni Järvinen (called LTRS for short) was quite a reasonable choice to be a testbed for the current formalisation both of lattices and of rough sets. A popular computerised proof-assistant Mizar was used as a tool, hence all the efforts are available in one of the largest repositories of computer-checked mathematical knowledge, called Mizar Mathematical Library.

Słowa kluczowe

EN

rough sets; lattice theory; mathematical proofs; binary system; set theory

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2016
• Tom: Vol. 147, nr 2/3
• Strony: 223--240
• Opis fizyczny: Bibliogr. 38 poz., tab.

Twórcy

autor

Grabowski A.

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

Bibliografia

• [1] Järvinen J. Lattice theory for rough sets. Transactions on Rough Sets, VI, Lecture Notes in Computer Science. 2007;4374:400–498. Available from: http://dx.doi.org/10.1007/978-3-540-71200-8_22. doi:10.1007/978-3-540-71200-8_22.
• [2] Zadeh LA. Fuzzy sets. Information and Control. 1965;8(3):338–353. Available from: http://dx.doi.org/10.1016/S0019-9958(65)90241-X. doi:10.1016/S0019-9958(65)90241-X.
• [3] Pawlak Z. Rough Sets: Theoretical Aspects of Reasoning about Data. Kluwer, Dordrecht; 1991. doi:10.1007/978-94-011-3534-4. ISBN: 978-0-7923-1472-1, 978-94-010-5564-2.
• [4] Wiedijk F. Formal proof—getting started. Notices of the American Mathematical Society. 2008;55(11):1408–1414.
• [5] Bryniarski E. Formal conception of rough sets. Fundamenta Informaticae. 1996;27(2/3):109–136. Available from: http://dx.doi.org/10.3233/FI-1996-272302. doi:10.3233/FI-1996-272302.
• [6] Bancerek G, Byliński C, Grabowski A, Korniłowicz A, Matuszewski R, Naumowicz A, et al. Mizar: state of-the-art and beyond. In: Kerber M, Carette J, Kaliszyk C, Rabe F, Sorge V, editors. Intelligent Computer Mathematics – International Conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Vol. 9150 of Lecture Notes in Computer Science. Springer; 2015, pp. 261–279. Available from: http://dx.doi.org/10.1007/978-3-319-20615-8_17. doi:10.1007/978-3-319-20615-8_17.
• [7] Bancerek G, Rudnicki P. A Compendium of Continuous Lattices in Mizar (formalizing recent mathematics). Journal of Automated Reasoning. 2002;29(3/4):189–224. Available from: http://dx.doi.org/10.1023/A:1021966832558. doi:10.1023/A:1021966832558.
• [8] Zhu W. Generalized rough sets based on relations. Information Sciences. 2007;177(22):4997–5011. Available from: http://dx.doi.org/10.1016/j.ins.2007.05.037. doi:10.1016/j.ins.2007.05.037.
• [9] Grätzer G. General Lattice Theory. Academic Press; 1978. ISBN: 008087391X, 9780080873916.
• [10] McCune W. Solution of the Robbins problem. Journal of Automated Reasoning. 1997;19(3):263–276. Available from: http://dx.doi.org/10.1023/A:1005843212881. doi:10.1023/A:1005843212881.
• [11] Grabowski A. Automated discovery of properties of rough sets. Fundamenta Informaticae. 2013;128(1-2):65–79. Available from: http://dx.doi.org/10.3233/FI-2013-933. doi:10.3233/FI-2013-933.
• [12] Grabowski A. Mechanizing complemented lattices within Mizar type system. Journal of Automated Reasoning. 2015;55(3):211–221. Available from: http://dx.doi.org/10.1007/s10817-015-9333-5. doi:10.1007/s10817-015-9333-5.
• [13] Pomykała J, Pomykała JA. The Stone algebra of rough sets. Bulletin of the Polish Academy of Sciences, Mathematics. 1988;36:495–508.
• [14] Pagliani P. Rough sets and Nelson algebras. Fundamenta Informaticae. 1996;27(2–3):205–219. Available from: http://dx.doi.org/10.3233/FI-1996-272308. doi:10.3233/FI-1996-272308.
• [15] Grabowski A. On the computer-assisted reasoning about rough sets. In: Dunin-Kęplicz B, Jankowski A, Skowron A, Szczuka M, editors. Monitoring, Security, and Rescue Techniques in Multiagent Systems. Vol. 28 of Advances in Soft Computing. Berlin, Heidelberg: Springer-Verlag; 2005, pp. 215–226. Available from: http://dx.doi.org/10.1007/3-540-32370-8_15. doi:10.1007/3-540-32370-8_15.
• [16] Grabowski A, Jastrzębska M. Rough set theory from a math-assistant perspective. In: Kryszkiewicz M, Peters JF, Rybiński H, Skowron A, editors. Rough Sets and Intelligent Systems Paradigms, International Conference, RSEISP 2007, Warsaw, Poland, June 28–30, 2007, Proceedings. Vol. 4585 of Lecture Notes in Computer Science. Springer; 2007, pp. 152–161. Available from: http://dx.doi.org/10.1007/978-3-540-73451-2_17. doi:10.1007/978-3-540-73451-2_17.
• [17] Iwiński TB. Algebraic approach to rough sets. Bulletin of the Polish Academy of Sciences, Mathematics. 1987;35:673–683.
• [18] Grabowski A, Korniłowicz A, Naumowicz A. Mizar in a nutshell. Journal of Formalized Reasoning. 2010;3(2):153–245. Available from: http://dx.doi.org/10.6092/issn.1972-5787/1980. doi:10.6092/issn.1972-5787/1980.
• [19] Naumowicz A, Korniłowicz A. A brief overview of Mizar. In: Berghofer S, Nipkow T, Urban C, Wenzel M, editors. Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics. Vol. 5674 of TPHOLs’09, Lecture Notes in Computer Science. Berlin, Heidelberg: Springer-Verlag; 2009, pp. 67–72. Available from: http://dx.doi.org/10.1007/978-3-642-03359-9_5. doi:10.1007/978-3-642-03359-9_5.
• [20] Korniłowicz A. Definitional expansions in Mizar. Journal of Automated Reasoning. 2015;55(3):257–268. Available from: http://dx.doi.org/10.1007/s10817-015-9331-7. doi:10.1007/s10817-015-9331-7.
• [21] Grabowski A. Efficient rough set theory merging. Fundamenta Informaticae. 2014;135(4):371–385. Available from: http://dx.doi.org/10.3233/FI-2014-1129. doi:10.3233/FI-2014-1129.
• [22] Harrison J. Formalized Mathematics. Technical Report 36, Turku Centre for Computer Science (TUCS). 1996; ISBN: 951-650-813-8.
• [23] Grabowski A. Two axiomatizations of Nelson algebras. Formalized Mathematics. 2015;23(2):115–125. Available from: http://dx.doi.org/10.1515/forma-2015-0012. doi:10.1515/forma-2015-0012.
• [24] Düntsch I. A logic for rough sets. Theoretical Computer Science. 1997;179(1–2):427–436. Available from: http://dx.doi.org/10.1016/S0304-3975(96)00334-9. doi:10.1016/S0304-3975(96)00334-9.
• [25] Järvinen J. Modal-like operators in Boolean lattices, Galois connections and fixed points. Fundamenta Informaticae. 2007;76(1–2):129–145. Available from: http://content.iospress.com/articles/fundamenta-informaticae/fi76-1-2-09.
• [26] Maddana Swamy U, Rao GC. Almost distributive lattices. Journal of Australian Mathematical Society. 1981;31:77–91. Available from: http://dx.doi.org/10.1017/S1446788700018498. doi:10.1017/S1446788700018498.
• [27] Isomichi Y. New concepts in the theory of topological space – supercondensed set, subcondensed set, and condensed set. Pacific Journal of Mathematics. 1971;38(3):657–668. Available from: http://dx.doi.org/10.2140/pjm.1971.38.657. doi:10.2140/pjm.1971.38.657.
• [28] Grabowski A. Formalization of generalized almost distributive lattices. Formalized Mathematics. 2014;22(3):257–267. Available from: http://dx.doi.org/10.2478/forma-2014-0026. doi:10.2478/forma-2014-0026.
• [29] Grabowski A. Stone lattices. Formalized Mathematics. 2015;23(4):387–396. Available from: http://dx.doi.org/10.1515/forma-2015-0031. doi:10.1515/forma-2015-0031.
• [30] Wiedijk F. The de Bruijn factor; 2010. Unpublished note. Available from: http://www.cs.ru.nl/~freek/factor/factor.pdf.
• [31] Naumowicz A. An example of formalizing recent mathematical results in Mizar. Journal of Applied Logic. 2006;4(4):396–413. Available from: http://dx.doi.org/10.1016/j.jal.2005.10.003. doi:10.1016/j.jal.2005.10.003.
• [32] Yao Y, Yao B. Covering based rough set approximations. Information Sciences. 2012;200:91–107. Available from: http://dx.doi.org/10.1016/j.ins.2012.02.065. doi:10.1016/j.ins.2012.02.065.
• [33] Yao YY. Two views of the rough set theory in finite universes. International Journal of Approximate Reasoning. 1996;15(4):291–317. Available from: http://dx.doi.org/10.1016/S0888-613X(96)00071-0. doi:10.1016/S0888-613X(96)00071-0.
• [34] Lamport L. How to write a proof. American Matematical Monthly. 1995;102(7):600–608.
• [35] Kühlwein D, Blanchette JC, Kaliszyk C, Urban J. MaSh: Machine Learning for Sledgehammer. In: Blazy S, Paulin-Mohring C, Pichardie D, editors. Interactive Theorem Proving 2013. Vol. 7998 of Lecture Notes in Computer Science. Springer-Verlag; 2013, pp. 35–50. Available from: http://dx.doi.org/10.1007/978-3-642-39634-2_6. doi:10.1007/978-3-642-39634-2_6.
• [36] Urban J, Sutcliffe G. Automated reasoning and presentation support for formalizing mathematics in Mizar. In: Blazy S, Paulin-Mohring C, Pichardie D, editors. Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010. Vol. 6167 of Lecture Notes in Computer Science. Springer-Verlag; 2010, pp. 132–146. Available from: http://dx.doi.org/10.1007/978-3-642-14128-7_12. doi:10.1007/978-3-642-14128-7_12.
• [37] Pąk K. Methods of lemma extraction in natural deduction proofs. Journal of Automated Reasoning. 2013;50(2):217–228. Available from: http://dx.doi.org/10.1007/s10817-012-9267-0. doi:10.1007/s10817-012-9267-0.
• [38] Alama J, Kohlhase M, Mamane L, Naumowicz A, Rudnicki P, Urban J. Licensing the Mizar Mathematical Library. In: Davenport JH, Farmer WM, Urban J, Rabe F, editors. Proceedings of the 18th Calculemus and 10th International Conference on Intelligent Computer Mathematics. Vol. 6824 of Lecture Notes in Computer Science. Berlin, Heidelberg: Springer-Verlag; 2011, pp. 149–163. Available from: http://dx.doi.org/10.1007/978-3-642-22673-1_11. doi:10.1007/978-3-642-22673-1_11.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).