Lattice Theory for Rough Sets - An Experiment in Mizar

Abstract

Rough sets is a well-known approach to incomplete or imprecise data. In the paper we briefly report how this framework was successfully encoded with the help of one of the leading computer proof assistants in the world. Thanks to their abstract and flexible character based essentially on binary relations, lattices as a basic viewpoint appeared a very feasible one in the case of rough sets. We 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. We 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 [11] (LTRS) was quite a reasonable choice to be a testbed for the current formalization both of lattices and of rough sets in Mizar.

-

Through the years ordinary set theory appeared not to be feasible enough for modelling incomplete or imprecise information. Even if basically built on top of Zermelo-Fraenkel widely accepted by most mathematicians, fuzzy sets by Zadeh [ 22 ] proposed new view for membership functions, where degree of membership taken from the unit interval was considered rather than classical discrete bipolarity. Pawlak’s alternative approach [ 16 ], although essentially of the same origin, was different – its probabilistic features were underlined. Also the focus was put rather on collective properties of clusters of objects than those of individuals as the latter can be hardly accessible.

Formalization is doing mathematics in a language formal enough to be understandable by computers [ 19 ] (of course, doing mathematics means also the act of proving theorems and correctness of definitions according to classical logic and Zermelo-Fraenkel set theory). This activity, obviously without the use of computers is dated back to Peano and Bourbaki as every mathematician uses more or less formal language [ 1 ]; but computer certification of mathematics can be useful for many reasons – machines open new possibilities of information analysis and exchange, they can help to discover new proofs or to shed some light on approaches from various perspectives; with the help of such automated proof assistants one can observe deeper connections between various areas of mathematics. For example, lattice theory delivers interesting and powerful algebraic model – useful in quantum theory, logic, linear algebra, and topology, to list only most popular ones. Hence it is not very surprising that also rough [ 11 ] and fuzzy set theories [ 22 ] can be modelled in this way. Studying connections between theories can be also benefitting to lattice theory itself – see [ 3 ] for the use of upper and lower rough ideals (filters) in a lattice.

The early works devoted to the formalization of mathematics with the help of automated proof assistants were not really connected with lattice theory. Checking Landau’s Grundlagen... was an experiment of translating arithmetic into AUTOMATH, one of the primary computerized proof-checkers. But first real widespread (at least for ordinary people) use of automated theorem provers was the solution of the Robbins problem (alternative axiomatization of Boolean algebras) with the help of EQP/Otter program by William McCune, which expressed the essence of computational power of computers in the area of equational proof search within lattice theory.

For years, there were essentially two types of activities in the computer certification of mathematics: either formal exploration of a single important theorem, in style of Kepler conjecture, or the computer encoding of a book or paper – all these aimed at building large formal repository of interconnected facts formally proven. In case of more compact research articles, the number of such efforts is quite big (even in the Mizar Mathematical Library (MML) there are at least twenty such encoded papers), but if the number of pages is relatively large, such projects are still rare.

The author was personally involved in the formalization projects of Compendium of Continuous Lattices (CCL) by Gierz et al. (approximately 70% done); he also provided more or less complete translations of papers into Mizar (Isomichi’s about classification of subsets of topological spaces, Zhu’s [ 23 ] on the approximation spaces based on arbitrary binary relations, and Rao’s on the generalized almost distributive lattices). The author of the present paper was interested in lattice theory, focusing on formalization issues of these structures with the help of automated proof-assistants of various kinds, including computerized theorem provers, dedicated software for calculations and visualization, and also computer algebra systems [ 4 ]. The idea of this work arose after having a look for Jouni Järvinen’s paper Lattice theory for rough sets [ 11 ] (which will be called LTRS in short), hence the title of the current paper is not accidental. Our short term goal is to provide annotated version of LTRS, where all items (definitions, propositions, and illustrative examples) will be mapped with their formal counterpart written in Mizar.

The structure of the paper is as follows: in the next section we introduce basic notions of lattice theory, also in mechanized setting, and discuss how it can be extended. Section 4 is devoted to concrete implementation of rough sets with Mizar system. The next section summarizes the pros and cons of our implementation and experiments with the Mizar Mathematical Library. We describe also the current state of injecting LTRS into MML. In the last section we draw some concluding remarks and plans for future. 2

Fundamentals of Lattice Theory

Lattices [ 10 ] are structures of the form

hL, ⊔, ⊓i, where L is a set (sometimes assumed to be non-empty), both binary operations ⊔ and ⊓ are commutative, associative, and satisfy the absorption laws. There is also an alternative definition of lattices as hL, ≤i, where ≤ is the partial ordering on L with the existence of suprema and infima for arbitrary pairs of elements of L. Essentially then, one can see lattices as hL, ⊔, ⊓, ≤i, where both parts are defined by one another.

It is worth noticing that lattices, especially those of them which have equational characterizations, can be automatically explored. Famous question on another axiomatization of Boolean algebras, known as the Robbins problem, was solved with EQP/OTTER system in 1996 after sixty years of unsuccessful human research. The first author provided also some proof developments in this problem, but with the use of another computer proof-assistant, namely the Mizar system [ 9 ]. It was created in the early seventies of the previous century in order to assist mathematicians in their work. Now the system consist of three main parts: the language in which all the mathematics can be expressed, close to the vernacular used by human mathematician, which at the same time can be automatically verified, the software which verifies the correctness of formalized knowledge in the classical logical framework, and last but not least, the huge collection of certified mathematical knowledge – the Mizar Mathematical Library (MML).

In Mizar formalism [ 9 ], lattices are structures of the form definition struct (/\-SemiLattRelStr, \/-SemiLattRelStr, LattStr)

LattRelStr

(# carrier -> set, L_join, L_meet -> (BinOp of the carrier),

InternalRel -> Relation of the carrier #); end; introduced by the first author to benefit from using binary operations and orderings at the same time. However, defining a structure we give only information about the signature – arities of operations and their results; specific axioms are needed additionally. Even if all of them can be freely used in their predicative variant, definitional expansions proved their usefulness. definition let L be non empty LattStr; attr L is meet-absorbing means :: LATTICES:def 8 for a,b being Element of L holds (a "/\" b) "\/" b = b; end;

The above is faithful translation of

∀a,b∈L (a ⊓ b) ⊔ b = b.

Continuing with all other axioms, we finally obtain lattices as corresponding structures with the collection of attributes under a common name Lattice-like. definition

mode Lattice is Lattice-like non empty LattStr; end;

The alternative approach to lattices through the properties of binary relations is a little bit different, so the underlying structure is just the set with InternalRel, namely RelStr. definition

mode Poset is reflexive transitive antisymmetric RelStr; end;

Boolean algebras, distributive lattices, and lattices with various operators of negation are useful both in logic and in mathematics as a whole, it is not very surprising that also rough set theory adopted some of the specific axiom sets – with Stone and Nelson algebras as most prominent examples.

The type LATTICE is, unlike the alternative approach where Lattice Mizar mode was taken into account, a poset with binary suprema and infima. Both approaches are in fact complementary, there is a formal correspondence between them shown, and even a common structure on which two of them are proved to be exactly the same. Why can ask the question why to have both approaches available in the repository of computer verified mathematical knowledge available at the same time? The simplest reason is that the ways of their generalizations vary; in case of posets we could use relational structures based on the very general properties of binary relations (even not necessarily more general, but just different – including equivalence relations or tolerances); equationally defined lattices are good starting point to consider e.g. semilattices or lattices with various additional operators – here also equational provers can show their deductive power. In this setting such important theorems as Stone’s representation theorem for Boolean algebras was originally formulated.

The operations of supremum and infimum are "\/" and "/\", respectively – in both approaches. The natural ordering is <= in posets and [= in lattices equationally defined. Note that c= is set-theoretical inclusion. The viewpoint of posets was extensively studied in Mizar during the big formalization project – translating into Mizar already mentioned CCL. 3

Extending Lattice Signature

From the informal point of view, the difference between the ordering given for hL, ⊔, ⊓i as

x ≤ y ⇔ x ⊔ y = y and posets defined as hL, ≤i where the existence of binary suprema and infima is axiomatically guaranteed is not very big. Here is the place for Leibniz’s Law (known also under the name of equality of indiscernibles or – slightly misleading – isomorphic copies). If it comes for real computerized proof-assistant, the problem arises. First of all, the choice of appropriate signature for lattices is important. On the one hand, we want to gather benefits from the use of sophisticated equational theorem provers, and hence equational characterization is strongly desirable. We can do so choosing lattice structure with two binary operations of supremum and infimum.

On the other hand however, one can use the properties of binary relations weaker than the partial ordering – either preorders or even, if we go further in the stream of reverse mathematics, arbitrary relations with certain properties. We can observe similar ideas in the theory of rough sets, with the example of Zhu’s papers [ 23 ], or topological spaces with various separation axioms.

All basic formalized definitions and theorems can be tracked under the address http://mizar.org.

4 Rough Sets and Approximation Spaces

Main disadvantage behind formalization of rough set theory [ 16 ] was that we had to choose among two basic approaches to rough sets: either as classes of equivalence relations (with further generalizations into tolerances or even arbitrary binary relations) or as pairs consisting of the lower and the upper approximation (see [ 7 ] for detailed description of approximation operators in Mizar). definition let X be Tolerance_Space, A be Subset of X; func RS A -> RoughSet of X equals :: INTERVA1:def 14

[LAp A, UAp A]; end;

The structure is defined as follows (_\/_ and _/\_ are taken componentwise): definition let X be Tolerance_Space; func RSLattice X -> strict LattStr means the carrier of it = RoughSets X & for A, B being Element of RoughSets X,

A1, B1 being RoughSet of X st A = A1 & B = B1 holds (the L_join of it).(A,B) = A1 _\/_ B1 & (the L_meet of it).(A,B) = A1 _/\_ B1; end; :: INTERVA1:def 23

We have proved formally that these structures are Lattice-like, distributive, and complete (arbitrary suprema and infima exist, not only binary ones). The properties are expressed in the form allowing automatic treatment of such structures. registration let X be Tolerance_Space;

cluster RSLattice X -> bounded complete; end;

Taking into account that [= is the ordering generated by the lattice operations, we can prove that it is just determined by the set-theoretical inclusion of underlying approximations. theorem :: INTERVA1:71 for X being Tolerance_Space, A, B being Element of RSLattice X,

A1, B1 being RoughSet of X st A = A1 & B = B1 holds A [= B iff

LAp A1 c= LAp B1 & UAp A1 c= UAp B1;

Detailed survey of the lattice-theoretical approach to rough sets is contained e.g. in Järvinen [ 11 ] paper, which enumerated some basic classes of lattices useful within rough set theory – e.g. Stone, de Morgan, Boolean lattices, and distributive lattices, to mention just the more general ones. All listed structures are well represented in the MML.

Flexibility of the Mizar language allows for defining new operators on already existing lattices without the requirement of repetitions of old structures, e.g. Nelson algebras are based on earlier defined de Morgan lattices (which are also of the more general interest), also defining various negation operators is possible in this framework. Furthermore, topological content widely represented in the Mizar Mathematical Library helped us to have illustrative projections into other areas of mathematics [ 5 ]. Here good example was (automatically discovered by us) linking with Isomichi classification of subsets of a topological space into three classes of subsets [ 6 ].

Recently we made some results in fuzzy numbers in formalized setting, and even if primarily we did not plan to include them here, LTRS forced us to do so. Namely, Example 141, p. 476 in LTRS is just the construction of L-fuzzy sets, so it seems we have to cover it also. Exactly just like in the case of rough sets (where we tried to stick to equivalence relations instead of the more general case), first formalization in Mizar had to be tuned to better reflect Zadeh’s mathematical idea [ 22 ]. The basic object RealPoset is a poset (a set equipped with the partial ordering, i.e. reflexive, transitive, and antisymmetric relation) – unit interval with the natural ordering defined of real numbers. We use Heyting algebras as they are naturally connected with L-fuzzy sets. We can define the product of the copies of the (naturally ordered) unit intervals (by the way, this was defined in Mizar article YELLOW_1 by the first author during the formalization of CCL). definition let A be non empty set; func FuzzyLattice A -> Heyting complete LATTICE equals :: LFUZZY_0:def 4 (RealPoset [. 0,1 .]) |^ A; end;

The above can be somewhat cryptic, however the next theorem explains how elements of the considered structure look like – these are just functions from A into the unit interval. theorem :: LFUZZY_0:14 for A being non empty set holds the carrier of FuzzyLattice A = Funcs (A, [. 0, 1 .]);

Although the lattice operations are not stated explicitly here (which could be a kind of advantage here), the ordering determines it uniquely via the natural ordering of real functions. The underlying structure is a complete Heyting algebra. Of course, the type of this Mizar functor is not only declarative – it had to be proved. theorem :: LFUZZY_0:19 for C being non empty set,

s,t being Element of FuzzyLattice C holds s "\/" t = max(@s, @t);

The functor @s returns for an element of the lattice of fuzzy sets the corresponding membership function (i.e. a fuzzy set). The so-called type cast is needed to properly recognize which operation max should be used – in our case it is the operation defined for arbitrary functions. Of course, in the above definition, A is an arbitrarily chosen non-empty set; it can be replaced by the carrier of a lattice, and the definition of FuzzyLattice A can be tuned accordingly. 5

Where Are We Now

At the beginning of expressing things fully formally, usually it is hard to estimate the real amount of needed work. The unreasonable delays are often caused by authors’ omissions in proof steps, where inferences suggested to be trivial appear to be hard or even false (we met some such situations during CCL project), references for papers yet classical in the literature of the subject (but absent in the formal repository, which has to be overworked), and some isomorphisms in the spirit of category theory (let us assume continuous mappings to be arrows in proper category) or logic (all we just considered is trivial in the framework of proper modal logic).

As basic stages of our work we could enumerate: – Choosing appropriate model for formalization – in CCL we decided to have two series, YELLOW (bridging the gap between the current state of MML and needed knowledge) and WAYBEL formalizing one-by-one items from the book. It appears however, that due to highly self-containing nature of LTRS a kind of YELLOW series practically vanishes and we will give rather a set of monographical articles (proofs from MML will be only linked, not rewritten). – Providing a platform for the work, with the aim of incorporating the work into the Mizar Mathematical Library (we want to make it available to other users making it distributed with every distribution of the Mizar system). – Wikipedia proved that in case of wide projects a model of Wiki for collective work wins with svn or cvs (concurrent version systems) with closed architecture (although a bit of centralized control to ensure the appropriateness of changes is definitely needed). – Back-revisions of the MML, as the Mizar repository can also benefit (generalizations, removing repetitions, making unifications). Here we mention also the possibility of proof reorganization: lemmas can be extracted, proof structure can be flattened, if possible, etc. – Translation of the Mizar source code into LATEX via available tools and comparing the differences with LTRS. During the process of printing the journal Formalized Mathematics which is a translation between vocabulary file and LATEX format given in XML; formats are once fixed, but it is no problem at all to get instead of UAp(A) the set A with the upper triangle (the notation used in LTRS), etc. Of course, alternatively one can define its own synonym, which does not bring any new semantical information. We can mention also hyperlinked version of articles, hence anyone can dig down to the fundamentals. – Statistical research on results, once we get complete formal translation. Hence besides explicit references, all connections can be listed – facts from mathematical folklore, informal omissions, detailed proof steps, and proof similarities.

As of now, we do not provide percentage of the real work done (we plan eventually to give a one-to-one correspondence between LTRS and MML, and as of now there is no fully annotated version accepted into the MML), but thorough insight into both sources results in the following numbers (see Table 1).

There are three items we should briefly explain: MML lacks the part devoted to Stone lattices (Chapter 4), although we have some 1500 lines of Mizar code covering most of the missing content. Although the chapter with Galois connections is covered in 70%, it is not very much used in the Mizar repository, hence low numbers in Chapter 9 and 10. Also information systems already formalized in Mizar need to be adjusted in order to provide smooth correspondence with reducts and rough sets. In total, nearly 70% of items are covered in the current MML. In the next table, we present most representative Mizar articles (MML identifiers, i.e. filenames) for every chapter.

The quotation from [ 11 ] “Prerequisites are minimal and the work is self-contained" was very important for us – as after the finish we will calculate the so-called de Bruijn factor which measures the ratio between the amount of formal text and its informal counterpart. It is often claimed that in the case of ordinary mathematical submission its de Bruijn factor is approximately four – but it would not be the case of LTRS, as it has many illustrative examples.

The enumeration is continuous and examples are present in this sequence (in CCL, some examples were not formalized by us as either they were needed to solve the exercises, or they had purely illustrative character). Essentially then, the numbers are not fully reflecting the real state of formalization. Similar situation was during formalization of CCL in Mizar, where C∗-algebras were used as one of the examples (and we did not touch it at all as it would require massive work within completely different area of mathematics we dealt with).

Many theorems and definitions are inline, i.e. they are not formulated as separate items. Extremal example here is the list of boolean properties of sets (some 17 properties collected in Proposition 1), which of course in the MML is of the form of 17 separate theorems. We could choose either between the corollary which is a conjunct of all these or mapping single LTRS item into multiple MML items.

Even at the first sight, among obvious notions from mathematical folklore, two basic objects are especially correlated with our area of research: partitions (resp. coverings in more general approach [ 24 ]) and intervals [ 20 ]. Querying MML, we discovered that lattices of partitions were formalized already pretty well, but to our big surprise, this was not the case of intervals, so we had to make some preparatory work by ourselves.

Instead of using the ordered pair of approximations, we can claim that both coordinates are just arbitrary objects, so that we can do just a little bit reverse mathematics. It happens even in the heart of rough set theory – correlation of indiscernibility relation properties with those of approximation operators in style of [ 23 ] or underlying lattice properties [ 11 ] could lead us to develop some general theory of mathematical objects. One of the significant matchings discovered automatically with the help of our work was that classification of rough sets basically coincides with that of objects described by Isomichi – first class objects are precisely crisp sets, second class – rough sets with non-empty boundary, so third class just vanishes in equivalence-based approximation space. Details of this correspondence can be found in [ 6 ].

During our project of making both formal approaches to incomplete information accessible in the Mizar Mathematical Library, an extensive framework was created, besides lattices of rough sets (and also of fuzzy sets). Its summary is shown in Table 3.

Table 3 lists our MML articles about rough sets (started with ROUGHS), while the first group contains some preliminary notions and properties needed for smooth further work. We listed only MML items of which we are authors – among nearly 1250 files written by over 250 people. The complete list could contain nearly 20 files containing about 40 thousand lines of Mizar code (so it is about 2% of the MML). Not all of them are tightly connected with the theory of rough sets – they expand the theory of intervals, topologies, relational structures, and – last but not least – lattices, to list more notable areas of mathematics.

Following Grätzer’s classical textbook [ 10 ] in Mizar, practically all chapters from Järvinen work are covered, maybe except Section 8 on information systems (reducts are poorly covered in Mizar, but e.g. the Mizar article about Armstrong systems on ordered sets was coauthored by Armstrong himself). Also the final section on lattices of rough sets is not sufficiently covered in the MML, because not all combinations of properties of binary relations were considered. Our personal perspective was that [ 11 ] was even better written from the viewpoint of a developer of MML. The fact is that the theory is much simpler than in CCL by Gierz et al. (and it is more self-contained), although a little bit painful – at least from the formal point of view – category theory was used in a similar degree. 6

Conclusions and Future Work

In order to widen the formal framework within the MML, we should construct more algebraic models both for rough and fuzzy sets (as the aforementioned Stone algebras). Although we underlined the possibility of using external provers, we already applied some automatic tools available in the Mizar system aiming at discovering alternative proofs [ 17 ] and unnecessary assumptions to generalize the approach (similarly to generalizing from equivalence into tolerance relations in case of rough sets).

It is hard to describe all the formalized work which was done during this project in such a short form; however we tried to outline the very basic constructions. We hope to demonstrate the working prototype of annotated version of LTRS during CS&P 2015 conference, and, of course, to incorporate it into the MML to be explored with the help of Mizar internal tools. We hope to spend about a year of work to finish it completely. Our work was very much inspired by Järvinen [ 11 ] and Zhu [ 23 ], although regular formalization of this topic started back in 2000, much before both these papers. Some copyright issues should be solved as the best solution is just to publish [ 11 ] with links pointing out to appropriate Mizar items and proofs. In the era of expanding open access model for research we hope some limitations can vanish – although some issues connected with the repositories of knowledge formalized with the help of computers are quite interesting [ 2 ] and GNU/Creative Commons model is promising.

Mizar code enables also the information exchange with other proof assistants through its XML intermediate format. Even if the Mizar code is relatively well readable, LATEX version and HTML script with expandable and fully hyperlinked proofs are available. All Mizar files are also translated into TPTP [ 18 ] (first order logic form which can serve as a direct input for Thousands of Problems for Theorem Provers) and this could be one of the fundamental gains for the rough set community.

References

1. Bryniarski E. : Formal conception of rough sets , Fundamenta Informaticae , 27 ( 2 /3), 109 - 136 ( 1996 )

2. Alama J. , Kohlhase M. , Mamane L. , Naumowicz A. , Rudnicki P. , Urban J .: Licensing the Mizar Mathematical Library, Proc. of MKM 2011 , LNCS (LNAI) 6824 , 149 - 163 ( 2011 )

3. Estaji A.A. , Hooshmandasl M.R. , Davvaz B. : Rough set theory applied to lattice theory , Information Sciences , 200 , 108 - 122 ( 2012 )

4. Grabowski A. : Mechanizing complemented lattices within Mizar type system , Journal of Automated Reasoning ( 2015 ), DOI: 10.1007/s10817-015-9333-5

5. Grabowski A. : Efficient rough set theory merging , Fundamenta Informaticae , 135 ( 4 ), 371 - 385 ( 2014 )

6. Grabowski A. : Automated discovery of properties of rough sets , Fundamenta Informaticae , 128 ( 1-2 ), 65 - 79 ( 2013 )

7. Grabowski A. : On the computer-assisted reasoning about rough sets, in Monitoring, Security and Rescue Techniques in Multiagent Systems, B. Dunin-Ke¸plicz, A . Jankowski, M. Szczuka (Eds.), Advances in Soft Computing , 28 , 215 - 226 ( 2005 )

8. Grabowski A. , Jastrze¸bska M. : Rough set theory from a math-assistant perspective, in Rough Sets and Intelligent Systems Paradigms , M. Kryszkiewicz , J. Peters , H. Rybin´ski (Eds.), Lecture Notes in Artificial Intelligence , 4585 , 152 - 161 ( 2007 )

9. Grabowski A. , Korniłowicz A. , Naumowicz A. : Mizar in a nutshell , Journal of Formalized Reasoning , 3 ( 2 ), 153 - 245 ( 2010 )

10. Grätzer G.: General Lattice Theory , Birkhäuser ( 1998 )

11. Järvinen J.: Lattice theory for rough sets, Transactions on Rough Sets VI, LNCS (LNAI) 4374 , 400 - 498 ( 2007 )

12. Kawahara Y. , Furusawa H.: An algebraic formalization of fuzzy relations , Fuzzy Sets and Systems , 101 , 125 - 135 ( 1999 )

13. Korniłowicz A. : On rewriting rules in Mizar , Journal of Automated Reasoning , 50 ( 2 ), 203 - 210 ( 2013 )

14. Moore R. , Lodwick W.: Interval analysis and fuzzy set theory , Fuzzy Sets and Systems , 135 ( 1 ), 5 - 9 ( 2003 )

15. Naumowicz A. , Korniłowicz A. : A brief overview of Mizar , in TPHOLs'2009, S. Berghofer et al. (Eds.), LNCS, 5674 , 67 - 72 ( 2009 )

16. Pawlak Z. : Rough Sets: Theoretical Aspects of Reasoning about Data , Kluwer, Dordrecht ( 1991 )

17. Pa ¸k K.: Methods of lemma extraction in natural deduction proofs , Journal of Automated Reasoning , 50 ( 2 ), 217 - 228 ( 2013 )

18. Urban J. , Sutcliffe G.: Automated reasoning and presentation support for formalizing mathematics in Mizar , LNCS, 6167 , Springer, 132 - 146 ( 2010 )

19. Wiedijk F.: Formal proof - getting started, Notices of the AMS , 55 ( 11 ), 1408 - 1414 ( 2008 )

20. Yao Y.Y. : Two views of the rough set theory in finite universes , International Journal of Approximate Reasoning , 15 ( 4 ), 291 - 317 ( 1996 )

21. Yao Y. , Yao B. : Covering based rough set approximations , Information Sciences , 200 , 91 - 107 ( 2012 )

22. Zadeh L.: Fuzzy sets , Information and Control , 8 ( 3 ), 338 - 353 ( 1965 )

23. Zhu W. : Generalized rough sets based on relations , Information Sciences , 177 ( 22 ), 4997 - 5011 ( 2007 )

24. Zhu W. : Topological approaches to covering rough sets , Information Sciences , 177 ( 6 ), 1499 - 1508 ( 2007 )