Affiliations: University of Białystok, Institute of Informatics, Akademicka 2, 15-267 Białystok, Poland. [email protected]
Note: [] The article is a revised and expanded version of the paper presented at the 22nd Workshop on Concurrency, Specification and Programming (CS&P 2013, Warsaw, Poland). Thanks go to the anonymous referees for kind remarks on the earlier version of the paper. These deep thoughts suggested us a closer look for connections between Isomichi's work and rough sets. Address for correspondence: University of Białystok, Institute of Informatics, Akademicka 2, 15-267 Białystok, Poland
Abstract: 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 proof-assistant. 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.
