Efficient Rough Set Theory Merging

• Autorzy: Grabowski A.

Identyfikatory

DOI

10.3233/FI-2014-1129

• Języki publikacji: EN

Abstrakty

EN

Theory exploration is a term describing the development of a formal approach to selected topic, usually within mathematics or computer science, with the help of an automated proofassistant. This activity however usually doesn’t reflect the view of science considered as a whole, not as separated islands of knowledge. Merging theories essentially has its primary aim of bridging these gaps between specific disciplines. As we provided formal apparatus for basic notions within rough set theory (as e.g. approximation operators and membership functions), we try to reuse the knowledge which is already contained in available repositories of computer-checked mathematical knowledge, or which can be obtained in a relatively easy way. We can point out at least three topics here: topological aspects of rough sets – as approximation operators have properties of the topological interior and closure; possible connections with formal concept analysis; lattice-theoretic approach giving the algebraic viewpoint (e.g. Stone algebras). In the first case, we discovered semiautomatically some connections with Isomichi’s classification of subsets of a topological space and with the problem of fourteen Kuratowski sets. This paper is also a brief description of the computer source code which is a feasible illustration of our approach – nearly two thousand lines containing all the formal proofs (essentially we omit them in the paper). In such a way we can give the formal characterization of rough sets in terms of topologies or orders. Although fully formal, still the approach can be revised to keep the uniformity all the time.

Słowa kluczowe

EN

rough sets; rough concept analysis; knowledge management; formal topology

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 135, nr 4
• Strony: 371--385
• Opis fizyczny: Bibliogr. 21 poz., rys.

Twórcy

autor

Grabowski A.

• University of Białystok, Institute of Informatics, Akademicka 2, 15-267 Białystok, Poland

Bibliografia

• [1] G. Bancerek, Development of the theory of continuous lattices in Mizar, in: M. Kerber and M. Kohlhase (eds.), The Calculemus-2000 Symposium Proceedings, pp. 65–80, 2001.
• [2] G. Bancerek, On the structure of Mizar types, in: H. Geuvers and F. Kamareddine (eds.), Proc. of MLC 2003, ENTCS 85(7), 2003.
• [3] W. Farmer, J. Guttman, and F. Thayer, Little theories, in: D. Kapur (ed.), Automated Deduction – CADE-11, LNCS 607, pp. 567–581, 1992.
• [4] A. Grabowski, Automated discovery of properties of rough sets, Fundamenta Informaticae, 128(1-2), pp. 65–79, 2013.
• [5] A. Grabowski, A. Korniłowicz, and A. Naumowicz, Mizar in a nutshell, Journal of Formalized Reasoning, 3(2), pp. 153–245, 2010.
• [6] A. Grabowski, Ch. Schwarzweller, Rough Concept Analysis – theory development in the Mizar system, MKM 2004 Proceedings, LNCS 3119, pp. 130–144, 2004.
• [7] A. Grabowski, Ch. Schwarzweller, Towards automatically categorizing mathematical knowledge, M. Ganzha, L. Maciaszek, and M. Paprzycki (Eds.), FedCSIS 2012 Proceedings, pp. 63–68, 2012.
• [8] Y. Isomichi, New concepts in the theory of topological space – supercondensed set, subcondensed set, and condensed set, Pacific Journal of Mathematics, 38(3), pp. 657–668, 1971.
• [9] J. Järvinen, Approximations and rough sets based on tolerances, in: W. Ziarko and Y. Yao (eds.), Proc. of RSCTC 2000, LNAI 2005, pp. 182–189, 2001.
• [10] R. E. Kent, Rough Concept Analysis: a synthesis of rough sets and formal concept analysis, Fundamenta Informaticae 27(2–3), pp. 169–181, 1996.
• [11] A. Naumowicz, A. Korniłowicz, A brief overview of Mizar, in S. Berghofer et al (eds.), Proc. of TPHOL 2009, Lecture Notes in Computer Science 5674, pp. 67–72, 2009.
• [12] T. Nipkow, L. Paulson, and M. Wenzel, Isabelle/HOL – a proof assistant for higher-order logic, LNCS 2283, 2002.
• [13] Z. Pawlak: Automatyczne dowodzenie twierdzeń, Warsaw, PZWS, 1965 (Eng. Automated theorem proving).
• [14] Z. Pawlak, Rough Sets: Theoretical Aspects of Reasoning about Data, Kluwer, Dordrecht, 1991.
• [15] K. Pąk, Methods of lemma extraction in natural deduction proofs, Journal of Automated Reasoning, 50(2), pp. 217–228, 2013.
• [16] J. Saquer, J. S. Deogun, Concept approximations based on rough sets and similarity measures, International Journal on Applications of Mathematics in Computer Science, 11(3), pp. 655–674, 2001.
• [17] Ch. Schwarzweller, Introduction to concept lattices, Formalized Mathematics, 7(2), pp. 233–242, 1998.
• [18] J. Urban, G. Sutcliffe, Automated reasoning and presentation support for formalizing mathematics in Mizar, Lecture Notes in Computer Science, 6167, pp. 132–146, 2010.
• [19] F. Wiedijk, Formal proof – getting started, Notices of the American Mathematical Society, 55(11), pp. 1408–1414, 2008.
• [20] Y. Y. Yao, A comparative study of fuzzy sets and rough sets, Inf. Sciences, 109(1-4), pp. 227–242, 1998.
• [21] O. Yaskorska, K. Budzynska, and M. Kacprzak, Proving propositional tautologies in a natural dialogue, Fundamenta Informaticae, 128(1–2), pp. 239–253, 2013.